K-user mailing list

["Zhang, Yi" <yzhng173 AT illinois.edu>]

https://github.com/kframework/k/blob/master/k-distribution/tutorial/1_k/4_imp%2B%2B/lesson_3/README.md

Basically you need to label the two rules and kompile with --transition

Yi

On Jun 6, 2017, at 10:23 PM, 钱璟 <qjq793437528 AT 163.com> wrote:

Hello Sir
I tried to study about the nondeterministic behaviors in k.
for example : i defined two rules to the symbol "+" as below
   rule I1 + I2  => I1 +Int I2
   rule I1 + I2  => I1 * Int I2
i expect that  random match and rewrite one rule during the execution.however it doesn't work.
with the command krun --search ,there is the only one solution rather than the expected situation.


the test example program is
int a, b;
a= 100;
b=2;
a= b+2;

the result is that there is the only solution , the rule in the first place was be matched and applied .

what's wrong about my definition or something else ?  

thanks for your help in advance