K-user mailing list

[Dwight Guth <dwight.guth AT runtimeverification.com>]

I believe the issue is that between K 3.0 and 3.5 we removed the LTL-hooks module from the list of default includes, and it's required by the model checker in both versions. Try adding the following requires/imports pair to the syntax module of your language.

requires "builtins/model-checker.k"

imports LTL-HOOKS

On Tue, Aug 4, 2015 at 3:00 AM, 朱晓冉 <zhuxrsandra AT 163.com> wrote:

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 mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user