K-user mailing list

[Traian Florin Șerbănuță <traian.serbanuta AT info.uaic.ro>]

Hi Cosmin,

Before getting into superheat/supercool, you actually have transition to help you :-)

Transition rules are those which become rewrite rules in Maude and thus yield transitions in the execution graph.

Superheat/Supercool are used to control non-determinism due to the order of evaluation of an operation:

 - superheat says I want to make a choice whether I heat one argument or another of a strict operator

 - supercool says I want to cool completely (or as much as possible) the current computation to be allowed to choose again with a superheat rule.

relevant videos from the tutorial:

http://www.kframework.org/index.php/Lesson_3,_IMP%2B%2B:_Tagging;_Superheat/Supercool_Kompilation_Options

for superheat and supercool

and the final part (~ starting with minute 8) of the Lesson_6 for IMP++ for transitions

http://www.kframework.org/index.php/Lesson_6,_IMP%2B%2B:_Adding/Deleting_Cells_Dynamically;_Configuration_Abstraction,_Part_2

hope that helps,

Traian

2013/10/3 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


_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user