k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

[[K-user] ] ERROR of LTL model checking of K 3.4

From: 璟临天下 <qjq793437528 AT 163.com>
To: k-user AT lists.cs.illinois.edu
Subject: [[K-user] ] ERROR of LTL model checking of K 3.4
Date: Mon, 19 Mar 2018 19:39:17 +0800 (CST)
Authentication-results: illinois.edu; spf=pass smtp.mailfrom=qjq793437528 AT 163.com; dkim=pass header.d=163.com header.s=s110527; dmarc=none

hello sir,

i installed the k-framework 3.4 on Ubuntu 16.04. And, i have tried the ltl model checking for a simple case in tutorial.

the command is : krun sum.imp --ltlmc TureLtl , the output is true which is correct.

however, when i run with
krun --output pretty -cARGV="(ListItem(\"./a.out\") .List)" --load-cfg tmp-kcc-in-ccqjqrxq_8V.bin -d /home/dexter/Desktop/c-semantics-3.4.0/dist/c11-nd-kompiled -cARGC=1 --ltlmc TrueLtl
the error happened and the log is below :
[Error] Critical: Parse error: Desired start symbol not found: LtlFormula
File: TrueLtl
Location: (0,0,0,0)

and i can run it after deleting the ltlmc of the command. what is wrong ? how to fix this problem ?

thanks
P.S. this command is generated by the kcc script.
yours

[[K-user] ] ERROR of LTL model checking of K 3.4, 璟临天下, 03/19/2018