k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

[[K-user] ] About LTL model checking

From: 朱晓冉 <zhuxrsandra AT 163.com>
To: k-user AT cs.uiuc.edu
Subject: [[K-user] ] About LTL model checking
Date: Tue, 3 Nov 2015 20:45:23 +0800

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