K-user mailing list

[Dorel Lucanu <dlucanu AT info.uaic.ro>]

Dear Sergio,

Thanks for your message.

There two problems in your definition related to the use of the model-checker:

1)  In order to be efficient, the tool does not transform all K rules into transitions. Therefore, you must tag some rules as transitions to have a model to check.
For instance, if you write your rule as
rule <k> doh S:String => .K ... </k>
     <moe> ... . => ListItem(S) </moe>
     [transition]
then the krun tool returns "true"  for
krun a.doh --ltlmc "TrueLtl"

Another option is to arbitrarily tag your rule,
rule <k> doh S:String => .K ... </k>
     <moe> ... . => ListItem(S) </moe>
     [sometag]
and use a krun command as
krun a.doh --transition="sometag" --ltlmc "TrueLtl"

The argument of the option --transition could a have a list of tags.

2. If you replace "TrueLtl" with "FalseLtl", then you get an error similar to that reported below. The reason is that the krun cannot display the counter-example.
When you use the model checker, try to disable the connection with the I/O server. If remove the attribute "stream="stdout"" from the cell <moe>, i.e., you write the configuration as
configuration <T>
                <k> $PGM:K </k>
             <moe> .List </moe>
              </T>

then you get the counter-example.

I hope this helps you.

Bests,
Dorel

On 6/13/13 12:34 PM, Sergio Maffeis wrote:

Hi,

if i write a simple string in the stdout stream, my k program will run correctly but crash the model checker. here's a minimalist example:

1. the file doh.k is my language definition, that just prints what follows the keyword doh. i compile it with 'kompile doh.k --transition="kripke"'

2. the file a.doh is an example that prints "duff". i run it with
'krun a.doh' and it works fine

3. the file maudeoutput.xml is what i get after running 'krun a.doh --ltlmc "TrueLtl"' and the error message is "[Error] Critical: Cannot parse result xml from maude. If you believe this to be in error, please file a bug and attach .k/krun/maudeoutput.xml"

please can somebody help, i'm totally stuck here.

Sergio

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