K-user mailing list

[Pawel Pietrzak <pawel.pietrzak AT ltu.se>]

Hi, 
Thanks for your reply. 
Looking forward to the fix :)  
Pawel



On Oct 12, 2012, at 4:59 PM, Rosu, Grigore wrote:

> 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