k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

Re: [[K-user] ] About LTL model checking

From: Dwight Guth <dwight.guth AT runtimeverification.com>
To: 朱晓冉 <zhuxrsandra AT 163.com>
Cc: "k-user AT cs.uiuc.edu" <k-user AT cs.uiuc.edu>
Subject: Re: [[K-user] ] About LTL model checking
Date: Wed, 4 Nov 2015 13:16:36 -0600

Hi, does `kast -s LtlFormula -e "<>Ltl TrueLtl"` generate the same error when you run it? If so, can you try importing the LTL-HOOKS module into your syntax module?

On Tue, Nov 3, 2015 at 6:45 AM, 朱晓冉 <zhuxrsandra AT 163.com> wrote:

Hi,

I came across some problem about LTL model checking with K framework.

When I ran the system using command “krun test —ltlmc “<>Ltl TrueLtl” ", an error occurred as the following :

[Error] Critical: Parse error: Syntax error near unexpected character '<'
Source: Command line: parameters
Location: (1,1,1,1)

But it’s correct for the command “krun test —ltlmc “TrueLtl” “. I have imported the LTL syntax module of my project. The version of K framework I’m using is 3.5.

Is there something that I have missed?

Many thanks!

Bests,

Xiaoran Zhu

[[K-user] ] About LTL model checking, 朱晓冉, 11/03/2015
- Re: [[K-user] ] About LTL model checking, Dwight Guth, 11/04/2015