k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

[K-user] model checking dekker.cink

From: Pawel Pietrzak <pawel.pietrzak AT ltu.se>
To: k-user AT cs.uiuc.edu
Subject: [K-user] model checking dekker.cink
Date: Fri, 12 Oct 2012 09:01:21 +0200
List-archive: <http://lists.cs.uiuc.edu/pipermail/k-user/>
List-id: <k-user.cs.uiuc.edu>

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] model checking dekker.cink, Pawel Pietrzak, 10/12/2012
- Re: [K-user] model checking dekker.cink, Rosu, Grigore, 10/12/2012
  - Re: [K-user] model checking dekker.cink, Pawel Pietrzak, 10/12/2012