[EBMC] LTL spec in SMV input file
27 views
Skip to first unread message
Marek Adamek
May 27, 2019, 5:13:23 AM5/27/19
to CProver Support
Hello,
According to the EBMC page (http://www.cprover.org/ebmc/) input can be passed and SMV file and properties can be described in LTL. I assume that in this case I should use LTLSPEC in SMV file. Unfortunaltely program fails at during parsing:
According to the EBMC page (http://www.cprover.org/ebmc/) input can be passed and SMV file and properties can be described in LTL. I assume that in this case I should use LTLSPEC in SMV file. Unfortunaltely program fails at during parsing:
Parsing /Users/marek/phd/files/mc/smv/kripke_random10_1_5_5000.smv
file[file] line 122: syntax error before `G'
PARSING ERROR
I attached the file with the example. This file works fine with NuSMV. My question is: is LTL supported. If yes, please let me know how to make this example to work.
I attached the file with the example. This file works fine with NuSMV. My question is: is LTL supported. If yes, please let me know how to make this example to work.
Thanks,
Marek
Reply all
Reply to author
Forward
0 new messages