Support both LTL+CTL verification

GoogleCodeExporter commented 8 years ago

Currently, our nusmv plugin support only verification of the CTLSPEC 
expressions. We need to support verification of LTLSPEC expressions as well.

Todo:
1. The popup menu item "Check CTL using nusmv" should be renamed to "Run NuSMV 
Verification".

2. NuSMV generator should generate "LTLSPEC" into the *.nusmv file

3. NuSMV tool should execute: check_ltlspec -o counterexample.xml (see also 
nusmv manual http://nusmv.fbk.eu/NuSMV/userman/v25/nusmv.pdf)

Original issue reported on code.google.com by viliam.s...@gmail.com on 14 Dec 2011 at 11:13

GoogleCodeExporter commented 8 years ago

Original comment by viliam.s...@gmail.com on 14 Dec 2011 at 11:15

Added labels: Component-FM

GoogleCodeExporter commented 8 years ago

the issue has been fixed

Original comment by rud...@gmail.com on 6 Jan 2012 at 1:22

GoogleCodeExporter commented 8 years ago

Original comment by rud...@gmail.com on 6 Jan 2012 at 1:22

Changed state: Closed

luisandresilva / reprotool

Support both LTL+CTL verification #68