add lab1 and lab2 exercises

README.md

@@ -1,3 +1,4 @@
-# cps-lab-exercises-2021
+# CPS - Lab Exercises - 2021 UNIPD
 
-CPS - Lab Exercises - 2021 UNIPD
+- Lab 1 
+- Lab 2 (2021-11-19)

lab1/README.md

@@ -0,0 +1,8 @@
+
+# CPS Lab 1 Exercise (2021-10-27)
+
+- Mariano Sciacco
+- Davide Farinelli
+
+
+

lab1/delay_inverter.smv

@@ -0,0 +1,28 @@
+MODULE delay(input)
+    -- Model of the delay component
+    VAR
+        x : boolean;
+    ASSIGN
+        init(x) := FALSE;
+        next(x) := input;
+    DEFINE
+        out := x;
+ 
+MODULE relay(input)
+    -- Model of the relay
+    DEFINE
+        out := input; 
+        
+MODULE inverter(input)
+    -- Model of the inverter
+    DEFINE
+        out := !input; 
+
+
+MODULE main
+    -- Composition of delay and inverter
+    VAR
+        del : delay(inv.out);
+        inv : inverter(del.out);
+        
+INVARSPEC inv.out = !del.out;

lab1/railroad.smv

@@ -0,0 +1,90 @@
+MODULE train(signal)
+    -- Model of the train
+    VAR
+        mode : {away, wait, bridge};
+        out : {none, arrive, leave};
+    ASSIGN
+        init(mode) := away;
+        out := case
+            mode = away     : {none, arrive};
+            mode = bridge   : {none, leave};
+            TRUE            : none;
+        esac;
+        next(mode) := case
+            mode = away & out = arrive      : wait;
+            mode = wait & signal = green    : bridge;
+            mode = bridge & out = leave     : away;
+            TRUE                            : mode;
+        esac;
+
+MODULE controller(out_w, out_e)
+    -- First model of the controller
+    VAR
+        west    : {green, red};
+        east    : {green, red};
+        nearw   : {0, 1};
+        neare   : {0, 1};
+    ASSIGN
+        init(west)  := red;
+        init(east)  := red;
+        init(nearw) := 0;
+        init(neare) := 0;
+        
+        next(neare) := case
+            out_e = arrive  : 1;
+            out_e = leave   : 0;
+            TRUE            : neare;
+        esac;
+
+        next(nearw) := case
+            out_w = arrive  : 1;
+            out_w = leave   : 0;    
+            TRUE            : nearw;
+        esac;
+        
+        next(east) := case
+            neare = 0                              : red;
+            neare = 1 & west = red                 : green;
+            TRUE                                   : east;
+        esac;
+        
+        next(west) := case
+            nearw = 0                               : red;
+            nearw = 1 & east = red & neare != 1     : green;
+            TRUE                                    : west;
+        esac;
+    DEFINE
+        signal_w := west;
+        signal_e := east;
+
+
+-- to test
+MODULE WestTrainMonitor(out_w, out_e, signal_w)
+    VAR 
+        state : {0,1,2,3};
+    ASSIGN
+        init(state) := 0;
+        next(state) := case
+            state = 0 & out_w = arrive : 1;
+            -- state = 0 : 0;
+            state = 1 & signal_w != green & out_e = leave : 2;
+            state = 1 & signal_w = green : 0;
+            -- state = 1 : 1;
+            state = 2 & signal_w != green & out_e = leave : 3;
+            state = 2 & signal_w = green : 0;
+            -- state = 2 : 2;
+            -- state = 3 : 3;
+            TRUE : state;
+        esac;
+
+
+MODULE main
+    -- Composition of train_W, train_E and controller
+    VAR
+        train_w : train(contr.signal_w);
+        train_e : train(contr.signal_e);
+        contr   : controller(train_w.out, train_e.out);
+        wtm     : WestTrainMonitor(train_w.out, train_e.out, contr.signal_w);
+        
+INVARSPEC !(train_w.mode = bridge & train_e.mode = bridge);
+INVARSPEC !(wtm.state = 3);

lab1/switch.smv

@@ -0,0 +1,25 @@
+MODULE main
+    -- Model of the switch
+    IVAR
+        press   : boolean;
+    VAR
+        mode    : {on, off};
+        x       : 0..15;
+    ASSIGN
+        init(mode) := off;
+        next(mode) := case
+            mode = off & press              : on;
+            mode = on & (press | x >= 10)   : off;
+            TRUE                            : mode;
+        esac;
+        init(x) := 0;
+        next(x) := case
+            mode = on & next(mode) = off    : 0;
+            mode = on & x < 10              : x + 1;
+            TRUE                            : x;
+        esac;
+        
+INVARSPEC x <= 10;
+INVARSPEC mode = off -> x = 0;
+INVARSPEC x < 10;
+INVARSPEC mode = off;

lab2/README.md

@@ -0,0 +1,11 @@
+
+# CPS Lab 2 Exercise (2021-11-19)
+
+- Mariano Sciacco
+- Federico Carboni
+- Davide Franzosi
+
+> Note: requires `cpp` to make NUSMV work (or just replace it manually)
+> Note 2: use `nusmv -pre cpp <file>` to invoke the pre-processor of CPP
+
+

lab2/exercise_1.smv

@@ -0,0 +1,35 @@
+-- Non-deterministic
+
+MODULE main
+    VAR
+        state: 1..4;
+    ASSIGN
+        init(state) := 3;
+        next(state) := case
+            state = 1 : 2;
+            state = 2 : 2;
+            state = 3 : {1, 2, 4};
+            state = 4 : 3;
+        esac;
+
+    DEFINE
+        a := case
+            state = 1 | state = 2 : FALSE;
+            TRUE : TRUE;
+        esac;
+        
+        b := case
+            state = 1 | state = 3 : FALSE;
+            TRUE : TRUE;
+        esac;
+    
+    LTLSPEC F b; -- true
+    LTLSPEC G a; -- false
+    LTLSPEC a U b; -- false
+    LTLSPEC a U X b; -- true
+    LTLSPEC G F b; -- true
+    LTLSPEC F G b; -- false
+
+    LTLSPEC !(G a); -- false
+    LTLSPEC !(a U b); -- false
+    LTLSPEC !(F G b); -- false

lab2/fifo-ltlmc.smv

@@ -0,0 +1,188 @@
+--=========================================================================
+-- 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];

lab2/fifo-properties.smv

@@ -0,0 +1,55 @@
+--=========================================================================
+-- Exercise 2
+--=========================================================================
+
+--=========================================================================
+-- PROPERTIES OF FIFO
+--=========================================================================
+-- This file is not a standalone NuSMV file: it is to be included in
+-- fifo.smv or fifo-fixed.smv.
+
+-- The LTL properties in this file are numbered.  To have
+-- NuSMV check just the property numbered <p>, run it with the added
+-- option -n <p>.
+
+---------------------------------------------------------------------------
+-- Section 2.1, LTL Properties
+---------------------------------------------------------------------------
+
+
+--0: (a)
+LTLSPEC G(!(empty & full));
+
+--1: (b)
+LTLSPEC (F G write & ! G F read) -> (F full);
+
+
+--2: (c)
+LTLSPEC G (F ((wr_data = 0ud1_1) & write & !full)) -> F (rd_data = 0ud1_1);
+
+
+--3: (d)
+LTLSPEC G (F ((wr_data = data1) & write & !full)) -> F (rd_data = data1);
+
+
+-- salvo gli esercizi in una repo e ve li mando
+-- thk
+
+--4: (e)
+LTLSPEC
+  TRUE;
+
+--5: (f)
+
+LTLSPEC
+  TRUE;
+
+---------------------------------------------------------------------------
+-- Section 2.2, LTL Property showing bug
+---------------------------------------------------------------------------
+
+--6:
+LTLSPEC
+  TRUE;
+
+

lab2/fifo.smv

@@ -0,0 +1,68 @@
+--=========================================================================
+-- Exercise 2
+--=========================================================================
+
+--=========================================================================
+-- Secs 2.1 and 2.2: Verifying and fixing a FIFO model
+--=========================================================================
+
+-- For Sec 2.1:
+-- Run NuSMV on this file.  At its end, it includes the fifo-properties.smv
+-- file where you should enter all the requested LTL and CTL properties.
+
+-- For Sec 2.2:
+-- 1. Make a copy named fifo-fixed.smv of this file fifo.smv.
+-- 2. Enter your fix to the bug in the model in fifo-fixed.smv.  Do not
+--    alter fifo.smv.
+
+#define DEPTH 5
+#define WIDTH 1
+#define WORD word[WIDTH]
+
+MODULE main
+  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];
+
+
+
+
+#include "fifo-properties.smv"