--========================================================================= -- FV 2017-18: Practical Exercise 1 --========================================================================= -- Student UUN: --========================================================================= -- PROPERTIES OF FIFO --========================================================================= -- This file is not a standalone NuSMV file: it is to be included in -- fifo.smv or fifo-fixed.smv. -- The CTL and LTL properties in this file are numbered. To have -- NuSMV check just the property numbered
, run it with the added -- option -n
.
-- NuSMV always numbers CTL properties first, so the numbers for the
-- LTL properties do not start from 0.
---------------------------------------------------------------------------
-- Section 3.2, Q1: LTL Properties
---------------------------------------------------------------------------
--2: (a)
LTLSPEC
TRUE;
--3: (b)
LTLSPEC
TRUE;
--4: (c)
LTLSPEC
TRUE;
--5: (d)
LTLSPEC
TRUE;
--6: (e)
LTLSPEC
TRUE;
--7: (f)
LTLSPEC
TRUE;
---------------------------------------------------------------------------
-- Section 3.2, Q2: CTL Properties
---------------------------------------------------------------------------
--0: (a)
CTLSPEC
TRUE;
--1: (b)
CTLSPEC
TRUE;
---------------------------------------------------------------------------
-- Section 3.3, Q1: LTL Property showing bug
---------------------------------------------------------------------------
--8:
LTLSPEC
FALSE;
---------------------------------------------------------------------------
-- Section 3.3, Q2: Description of counter example behaviour
---------------------------------------------------------------------------
--