Sidebar

Main

Internal

Trace:

Differences

This shows you the differences between two versions of the page.

--- pn2mc:pt_cp_model_checking [2014/11/24 23:28]
jbiernacki [Problem]
+++ pn2mc:pt_cp_model_checking [2021/09/23 08:51] (current)
@@ Line 179: / Line 179: @@
 <code>
-NuSMV > check_ltlspec
+nuXmv > check_ltlspec
 -- specification G ( F p5) is false
 -- as demonstrated by the following execution sequence
@@ Line 218: / Line 218: @@
 -- specification G (((((!p0 & !p1) & !p2) & !p3) & !p4) -> ((((p5 | p6) |
 p7) | p8) | p9)) is true
-NuSMV > check_ctlspec
+nuXmv > check_ctlspec
 -- specification EF p5 is true
 -- specification EF p6 is true
@@ Line 272: / Line 272: @@
 ==== nuXmv ====
-----
+Using PetriNet2ModelChecker to translate reachability graph into description of the system in nuXmv code, the following file was generated:
+<code>
+MODULE main
+VAR
+	s: {s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12};
+	P5_client : 0..2;
+	P6_bufSpace : 0..2;
+	P4_client : 0..2;
+	P1_factory : 0..2;
+	P3_bufSpace : 0..2;
+	P2_factory : 0..2;
+ASSIGN
+	init(s) := s1;
+	next(s) := case
+		s = s1 : s2;
+		s = s2 : s3;
+		s = s3 : {s5, s4};
+		s = s4 : {s7, s6};
+		s = s5 : {s1, s7};
+		s = s6 : {s8, s9};
+		s = s7 : {s2, s9};
+		s = s8 : s10;
+		s = s9 : {s3, s10};
+		s = s10 : {s4, s11};
+		s = s11 : {s6, s12};
+		s = s12 : s8;
+	esac;
+	P5_client := case
+		s = s10 : 1;
+		s = s11 : 1;
+		s = s5 : 1;
+		s = s9 : 1;
+		s = s7 : 1;
+		s = s12 : 1;
+		TRUE : 0;
+	esac;
+	P6_bufSpace := case
+		s = s10 : 1;
+		s = s1 : 2;
+		s = s4 : 1;
+		s = s2 : 2;
+		s = s5 : 2;
+		s = s9 : 1;
+		s = s7 : 2;
+		s = s3 : 1;
+		TRUE : 0;
+	esac;
+	P4_client := case
+		s = s1 : 1;
+		s = s8 : 1;
+		s = s6 : 1;
+		s = s4 : 1;
+		s = s2 : 1;
+		s = s3 : 1;
+		TRUE : 0;
+	esac;
+	P1_factory := case
+		s = s11 : 1;
+		s = s1 : 1;
+		s = s6 : 1;
+		s = s5 : 1;
+		s = s9 : 1;
+		s = s3 : 1;
+		TRUE : 0;
+	esac;
+	P3_bufSpace := case
+		s = s10 : 1;
+		s = s11 : 2;
+		s = s8 : 2;
+		s = s6 : 2;
+		s = s4 : 1;
+		s = s9 : 1;
+		s = s12 : 2;
+		s = s3 : 1;
+		TRUE : 0;
+	esac;
+	P2_factory := case
+		s = s10 : 1;
+		s = s8 : 1;
+		s = s4 : 1;
+		s = s2 : 1;
+		s = s7 : 1;
+		s = s12 : 1;
+		TRUE : 0;
+	esac;
+</code>
+To verify specified properties of the system, the following LTL formulae were created:
+  - Consumer do not try to receive data from empty buffer, \\ \\ ''(P3_bufSpace = 0 Λ P4_client = 1) ⇒ ¬X(P5_client = 1)'' \\ \\
+  - Producer do not try to send data to full buffer, \\ \\ ''(P6_bufSpace = 0 Λ P2_factory = 1) ⇒ ¬X(P1_factory = 1)'' \\ \\
+  - There is no possibility of starvation of a consumer, \\ \\ ''GF(P4_client = 1) ⇒ GF(P5_client = 1)'' \\ \\
+  - There is no possibility of starvation of a producer, \\ \\ ''GF(P2_factory = 1) ⇒ GF(P1_factory = 1)'' \\ \\
+  - There are no deadlocks \\ \\ ''GF(P2_factory = 1) Λ GF(P1_factory = 1) Λ GF(P4_client = 1) Λ GF(P5_client = 1)'' \\ \\
+These formulae can be added to the previously generated nuXmv code for the model:
+<code>
+LTLSPEC (P3_bufSpace=0 & P4_client=1) -> !X(P5_client=1)
+LTLSPEC (P6_bufSpace=0 & P2_factory=1) -> !X(P1_factory=1)
+LTLSPEC G F (P4_client=1) -> G F (P5_client=1)
+LTLSPEC G F (P2_factory=1) -> G F (P1_factory=1)
+LTLSPEC G F (P2_factory=1) & G F (P1_factory=1) & G F (P4_client=1) &  G F (P5_client=1)
+</code>
+Verification of satisfiability of these formulae can be performed in nuXmv tool:
+<code>
+nuXmv > check_ltlspec
+-- specification ( G ( F P4_client = 1) -> G ( F P5_client = 1)) is true
+-- specification ( G ( F P2_factory = 1) -> G ( F P1_factory = 1)) is true
+-- specification ((P3_bufSpace = 0 & P4_client = 1) -> !( X P5_client = 1))
+is true
+-- specification ((P6_bufSpace = 0 & P2_factory = 1) -> !( X P1_factory =
+)) is true
+-- specification ((( G ( F P2_factory = 1) & G ( F P1_factory = 1)) & G ( F
+P4_client = 1)) & G ( F P5_client = 1)) is true
+</code>
+----
 ==== CADP ====