K-user mailing list

[Cosmin Radoi <cos AT illinois.edu>]

Hello,

I'm trying to figure out how the model checking/search mode works for k. My 
assumption was that it simply uses the underlying maude search. In this case, 
I would assume that superheating/supercooling rules are converted to maude 
rewrite rules. Still, the generated maude code for the rules in this small 
example uses equations.

module TEST
  syntax Bla ::= "a" | "b" | "c"  

  rule a => b   [supercool]
  rule a => c   [supercool]
endmodule

Furthermore, starting from the k program "a", I only get the solution "b". I 
expected both "b" and "c" as solutions. It seems that I somehow misunderstand 
the way k search works. Maybe I have a maude-tainted way of seeing things. I 
was assuming that each configuration is a state.

Where am I going off track?

Thanks,

Cosmin