kframework / k-legacy

The K tools (deprecated, see README)
http://kframework.org
Other
146 stars 61 forks source link

rule keeps getting applied but has no effect #2352

Open kheradmand opened 6 years ago

kheradmand commented 6 years ago

I have a configuration like following:

<T> <k> @resetArrays ( SetItem ( extra ) ) ~>  ... </k>
...
<arrays> extra |-> $array ( 4 , 0 , -1 ) </arrays>

And I have the following rules:

syntax KItem ::= "@resetArrays" "(" Set ")"
rule <k> @resetArrays((SetItem(N:InstanceName) => .Set) _:Set) ... </k>
     <arrays> (N |-> $array(_:Int , (_:Int => 0), (_:Int => -1))) _:Map </arrays>
rule <k> @resetArrays(.Set) => .K ... </k>

The first rule keeps getting applied (forever) but the resulting configuration does not change.