k-user AT lists.cs.illinois.edu
Subject: K-user mailing list
List archive
- From: 朱晓冉 <zhuxrsandra AT 163.com>
- To: k-user AT cs.uiuc.edu
- Subject: [K-user] About LTL model checking
- Date: Tue, 4 Aug 2015 16:00:45 +0800
- List-archive: <http://lists.cs.uiuc.edu/pipermail/k-user/>
- List-id: <k-user.cs.uiuc.edu>
Hi,
I have a stupid question but it held the key to my work. I wonder how to do LTL model checking using K framework with version 3.5.1.
When I ran the system using command “ krun test.imp --ltlmc “TrueLtl” ", an error occurred like the following:
[Error] Critical: The start symbol must be declared in the definition. Found: LtlFormula
However, this command can run correctly using K framework with version 3.0. Is there something that I have missed?
Many Thanks !
Bests,
Xiaoran Zhu
- [K-user] About LTL model checking, 朱晓冉, 08/04/2015
- Re: [[K-user] ] [K-user] About LTL model checking, Dwight Guth, 08/10/2015
Archive powered by MHonArc 2.6.16.