K-user mailing list

["Rosu, Grigore" <grosu AT illinois.edu>]

Hi Pawel,

I'm affraid the LTL model checker is broken right now ... We are in the 
middle of a transition to Java, and we ported things from the previous 
version of the tool on a by need basis.  But now we have a need :)  You will 
hear from us soon, hopefully telling you that it is fixed.

In the meanwhile, you can use the --search option of krun.  This allows you 
to see the entire state-space of a (finite-state) program.  Unfortunately, 
you do need the model checker if you want to check that state-space against 
temporal properties.

Sorry about that,
Grigore



________________________________________
From: 
k-user-bounces AT cs.uiuc.edu
 
[k-user-bounces AT cs.uiuc.edu]
 on behalf of Pawel Pietrzak 
[pawel.pietrzak AT ltu.se]
Sent: Friday, October 12, 2012 2:01 AM
To: 
k-user AT cs.uiuc.edu
Subject: [K-user] model checking dekker.cink

Hi all,

I am just discovering the K tool, and I think it's truly awesome! Thanks all 
the developers
for the great job!

However, I am having troubles with model checking dekker.cink  from the 
distribution:

krun programs/dekker.cink --ltlmc "LTL[] (eqTo(critical1, 1) LTL-> 
eqTo(critical2, 0))"


for which maude reports the following errors:

Warning: "maude_in8689419070254826136.maude", line 11: bad token KItem`(_`).
Warning: "maude_in8689419070254826136.maude", line 11: no parse for term.


Is this is a known issue? Is there an easy workaround?

Best,
Pawel


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