K-user mailing list

["Saxena, Manasvi" <msaxena2 AT illinois.edu>]

Hi Daniel,

I’m not entirely sure what you mean by modifying the path condition - If 
you’re representing the path condition as a cell in your semantics, then the 
rule you mentioned should work in K 4.0. However, it seems like you want a 
way to somehow grab the path condition from the execution. Unfortunately, at 
the moment, even though you can view the path condition during execution, 
there’s no way to match on it. However, we’re working towards implementing 
matching logic in K, which would allow us to match on the path condition. 

My suggestion would be to store the path condition in a special cell, and 
give semantics to its contents. That’d require you to make changes to the 
existing semantics, to have a the path condition put into your cell, every 
time a a rule with a requires clause applies. 

For instance - 

rule if B then S1 else S2 => #setPathConditionTrue ~> S1 … requires B >Int 0

rule if B then S1 else S2 => #setPathConditionFalse ~> S2 … requires B <=Int 0

rule <k> #setPathConditionTrue => . </k> <path-condition> _ => 1 
</path-condition>


Now you can make the #setPathCondition term take arguments , and make the 
<path-condition> cell a list of accumulated conditions. Note that 
#setPathCondition and the <path-conidition> cell are not constructs defined 
in K. You’d have to add them to you definition, and give them semantics. 


I hope this helps. Let me know if you have other questions. 

Manasvi
  
> On Feb 17, 2017, at 4:55 AM, 
> daparpon AT dsic.upv.es
>  wrote:
> 
> Thanks, I tried it and it works perfectly now. I have one more question,
> though: is it possible somehow to read (and/or modify) the path condition at
> run time, inside the rules of the language? For instance, in K 3.4 we were
> able to do something like this:
> 
> rule <path-condition> PC </path-condition> <k> [some term] => PC ... </k>
> 
> Is this possible in K 4.0? How could we do that?
> 
> Daniel