189 lines
6.3 KiB
Plaintext
189 lines
6.3 KiB
Plaintext
--=========================================================================
|
|
-- Exercise 3: Demonstration of LTL Model checking principles
|
|
--=========================================================================
|
|
|
|
--=========================================================================
|
|
-- Composition of system with a Buchi Automaton for negated property
|
|
--=========================================================================
|
|
|
|
MODULE main
|
|
VAR
|
|
sys : system;
|
|
nfba : neg_fmla_ba(sys.write, sys.full);
|
|
|
|
--=========================================================================
|
|
-- Emulation of a Buchi Automaton for negated property
|
|
--=========================================================================
|
|
|
|
---------------------------------------------------------------------------
|
|
-- Exercise 3, (a):
|
|
---------------------------------------------------------------------------
|
|
-- <NEGATED FORMULA, IN NORMALISED FORM>
|
|
|
|
---------------------------------------------------------------------------
|
|
-- Exercise 3, (b):
|
|
---------------------------------------------------------------------------
|
|
-- Complete the module that emulates a Buchi Automaton for !phi. An LTL
|
|
-- property capturing the acceptance condition for the automaton is asked for
|
|
-- separately below.
|
|
|
|
MODULE neg_fmla_ba(write, full)
|
|
VAR
|
|
st : 0 .. 3; -- <ADJUST NUMBER OF STATES, AS NEEDED>
|
|
ASSIGN
|
|
init(st) := 0;
|
|
next(st) := 0; -- <ADAPT AS NEEDED>
|
|
|
|
---------------------------------------------------------------------------
|
|
-- Exercise 4, (c):
|
|
---------------------------------------------------------------------------
|
|
-- Add a property here that, if true, captures that there are *no*
|
|
-- accepting runs of the automaton.
|
|
|
|
LTLSPEC TRUE;
|
|
|
|
--=========================================================================
|
|
-- FIFO model
|
|
--=========================================================================
|
|
|
|
#define DEPTH 5
|
|
#define WIDTH 1
|
|
#define WORD word[WIDTH]
|
|
|
|
MODULE system
|
|
VAR
|
|
-- Internal state
|
|
buffer : array 0 .. (DEPTH-1) of WORD;
|
|
rd_p: 0 .. DEPTH-1;
|
|
wr_p: 0 .. DEPTH-1;
|
|
empty : boolean; -- Also an output.
|
|
-- Inputs
|
|
write : boolean;
|
|
wr_data : WORD;
|
|
read : boolean;
|
|
|
|
FROZENVAR
|
|
-- For use in specifications to capture and refer to data values
|
|
data1 : WORD;
|
|
data2 : WORD;
|
|
DEFINE
|
|
-- Outputs
|
|
full := !empty & (rd_p = wr_p);
|
|
rd_data := buffer[rd_p];
|
|
ASSIGN
|
|
init(rd_p) := 0;
|
|
init(wr_p) := 0;
|
|
init(empty) := TRUE;
|
|
-- No init statement for buffer. Values in buffer at start
|
|
-- left unconstrained.
|
|
|
|
next(rd_p) := read & !empty ? (rd_p + 1) mod DEPTH : rd_p;
|
|
next(wr_p) := write & !full ? (wr_p + 1) mod DEPTH : wr_p;
|
|
|
|
next(empty) :=
|
|
case
|
|
empty & write : FALSE;
|
|
(rd_p + 1) mod DEPTH = wr_p & read: TRUE;
|
|
TRUE : empty;
|
|
esac;
|
|
|
|
next(buffer[0]) := wr_p = 0 & write & !full ? wr_data : buffer[0];
|
|
next(buffer[1]) := wr_p = 1 & write & !full ? wr_data : buffer[1];
|
|
next(buffer[2]) := wr_p = 2 & write & !full ? wr_data : buffer[2];
|
|
next(buffer[3]) := wr_p = 3 & write & !full ? wr_data : buffer[3];
|
|
next(buffer[4]) := wr_p = 4 & write & !full ? wr_data : buffer[4];
|
|
--=========================================================================
|
|
-- Exercise 3: Demonstration of LTL Model checking principles
|
|
--=========================================================================
|
|
|
|
--=========================================================================
|
|
-- Composition of system with a Buchi Automaton for negated property
|
|
--=========================================================================
|
|
|
|
MODULE main
|
|
VAR
|
|
sys : system;
|
|
nfba : neg_fmla_ba(sys.write, sys.full);
|
|
|
|
--=========================================================================
|
|
-- Emulation of a Buchi Automaton for negated property
|
|
--=========================================================================
|
|
|
|
---------------------------------------------------------------------------
|
|
-- Exercise 3, (a):
|
|
---------------------------------------------------------------------------
|
|
-- <NEGATED FORMULA, IN NORMALISED FORM>
|
|
|
|
---------------------------------------------------------------------------
|
|
-- Exercise 3, (b):
|
|
---------------------------------------------------------------------------
|
|
-- Complete the module that emulates a Buchi Automaton for !phi. An LTL
|
|
-- property capturing the acceptance condition for the automaton is asked for
|
|
-- separately below.
|
|
|
|
MODULE neg_fmla_ba(write, full)
|
|
VAR
|
|
st : 0 .. 3; -- <ADJUST NUMBER OF STATES, AS NEEDED>
|
|
ASSIGN
|
|
init(st) := 0;
|
|
next(st) := 0; -- <ADAPT AS NEEDED>
|
|
|
|
---------------------------------------------------------------------------
|
|
-- Exercise 4, (c):
|
|
---------------------------------------------------------------------------
|
|
-- Add a property here that, if true, captures that there are *no*
|
|
-- accepting runs of the automaton.
|
|
|
|
LTLSPEC TRUE;
|
|
|
|
--=========================================================================
|
|
-- FIFO model
|
|
--=========================================================================
|
|
|
|
#define DEPTH 5
|
|
#define WIDTH 1
|
|
#define WORD word[WIDTH]
|
|
|
|
MODULE system
|
|
VAR
|
|
-- Internal state
|
|
buffer : array 0 .. (DEPTH-1) of WORD;
|
|
rd_p: 0 .. DEPTH-1;
|
|
wr_p: 0 .. DEPTH-1;
|
|
empty : boolean; -- Also an output.
|
|
-- Inputs
|
|
write : boolean;
|
|
wr_data : WORD;
|
|
read : boolean;
|
|
|
|
FROZENVAR
|
|
-- For use in specifications to capture and refer to data values
|
|
data1 : WORD;
|
|
data2 : WORD;
|
|
DEFINE
|
|
-- Outputs
|
|
full := !empty & (rd_p = wr_p);
|
|
rd_data := buffer[rd_p];
|
|
ASSIGN
|
|
init(rd_p) := 0;
|
|
init(wr_p) := 0;
|
|
init(empty) := TRUE;
|
|
-- No init statement for buffer. Values in buffer at start
|
|
-- left unconstrained.
|
|
|
|
next(rd_p) := read & !empty ? (rd_p + 1) mod DEPTH : rd_p;
|
|
next(wr_p) := write & !full ? (wr_p + 1) mod DEPTH : wr_p;
|
|
|
|
next(empty) :=
|
|
case
|
|
empty & write : FALSE;
|
|
(rd_p + 1) mod DEPTH = wr_p & read: TRUE;
|
|
TRUE : empty;
|
|
esac;
|
|
|
|
next(buffer[0]) := wr_p = 0 & write & !full ? wr_data : buffer[0];
|
|
next(buffer[1]) := wr_p = 1 & write & !full ? wr_data : buffer[1];
|
|
next(buffer[2]) := wr_p = 2 & write & !full ? wr_data : buffer[2];
|
|
next(buffer[3]) := wr_p = 3 & write & !full ? wr_data : buffer[3];
|
|
next(buffer[4]) := wr_p = 4 & write & !full ? wr_data : buffer[4];
|