diff --git a/README.md b/README.md index d539d5e..aa467fa 100644 --- a/README.md +++ b/README.md @@ -1,3 +1,4 @@ -# cps-lab-exercises-2021 +# CPS - Lab Exercises - 2021 UNIPD -CPS - Lab Exercises - 2021 UNIPD \ No newline at end of file +- Lab 1 +- Lab 2 (2021-11-19) diff --git a/lab1/README.md b/lab1/README.md new file mode 100644 index 0000000..61a7c06 --- /dev/null +++ b/lab1/README.md @@ -0,0 +1,8 @@ + +# CPS Lab 1 Exercise (2021-10-27) + +- Mariano Sciacco +- Davide Farinelli + + + diff --git a/lab1/delay_inverter.smv b/lab1/delay_inverter.smv new file mode 100644 index 0000000..fe0f598 --- /dev/null +++ b/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; \ No newline at end of file diff --git a/lab1/ex_lab01.pdf b/lab1/ex_lab01.pdf new file mode 100644 index 0000000..47d2119 Binary files /dev/null and b/lab1/ex_lab01.pdf differ diff --git a/lab1/railroad.smv b/lab1/railroad.smv new file mode 100644 index 0000000..ddebc3f --- /dev/null +++ b/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); \ No newline at end of file diff --git a/lab1/switch.smv b/lab1/switch.smv new file mode 100644 index 0000000..5c09c8c --- /dev/null +++ b/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; \ No newline at end of file diff --git a/lab2/README.md b/lab2/README.md new file mode 100644 index 0000000..ba45eaa --- /dev/null +++ b/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 ` to invoke the pre-processor of CPP + + diff --git a/lab2/ex_lab02.pdf b/lab2/ex_lab02.pdf new file mode 100644 index 0000000..cc2cd5d Binary files /dev/null and b/lab2/ex_lab02.pdf differ diff --git a/lab2/exercise_1.smv b/lab2/exercise_1.smv new file mode 100644 index 0000000..4d06d3e --- /dev/null +++ b/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 \ No newline at end of file diff --git a/lab2/fifo-ltlmc.smv b/lab2/fifo-ltlmc.smv new file mode 100644 index 0000000..540e3b8 --- /dev/null +++ b/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): +--------------------------------------------------------------------------- +-- + +--------------------------------------------------------------------------- +-- 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; -- + ASSIGN + init(st) := 0; + next(st) := 0; -- + +--------------------------------------------------------------------------- +-- 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): +--------------------------------------------------------------------------- +-- + +--------------------------------------------------------------------------- +-- 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; -- + ASSIGN + init(st) := 0; + next(st) := 0; -- + +--------------------------------------------------------------------------- +-- 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]; diff --git a/lab2/fifo-properties.smv b/lab2/fifo-properties.smv new file mode 100644 index 0000000..c921f92 --- /dev/null +++ b/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

, run it with the added +-- option -n

. + +--------------------------------------------------------------------------- +-- 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; + + diff --git a/lab2/fifo.smv b/lab2/fifo.smv new file mode 100644 index 0000000..5d42c22 --- /dev/null +++ b/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"