Skip to content

Commit

Permalink
added pacemaker code
Browse files Browse the repository at this point in the history
  • Loading branch information
@codelion
codelion committed Oct 3, 2013
1 parent 51dd1a9 commit 7e91259
Show file tree
Hide file tree
Showing 27 changed files with 4,401 additions and 0 deletions.
148 changes: 148 additions & 0 deletions verified_pacemaker/AAI.ltl
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,148 @@
#define p sena == 1
#define q pula == 0
#define r avdelay == 0
#define s lastpacedpulsea == timer

/*
* Formula As Typed: [] (p -> <> (q && r && s))
* The Never Claim Below Corresponds
* To The Negated Formula !([] (p -> <> (q && r && s)))
* (formalizing violations of the original)
*/

never { /* !([] (p -> <> (q && r && s))) */
T0_init:
if
:: (((! ((q)) && (p)) || (((! ((r)) && (p)) || (! ((s)) && (p)))))) -> goto accept_S3
:: (1) -> goto T0_init
fi;
accept_S3:
if
:: (((! ((q))) || (((! ((r))) || (! ((s))))))) -> goto accept_S3
fi;
}

#ifdef NOTES
Use Load to open a file or a template.






#endif
#ifdef RESULT
warning: for p.o. reduction to be valid the never claim must be stutter-invariant
(never claims generated from LTL formulae are stutter-invariant)
depth 0: Claim reached state 5 (line 291)
depth 1233: Claim reached state 9 (line 296)
depth 1805: Claim reached state 9 (line 296)

(Spin Version 5.2.5 -- 17 April 2010)
+ Partial Order Reduction

Full statespace search for:
never claim +
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)

State-vector 96 byte, depth reached 3172, errors: 0
2534 states, stored (3484 visited)
1898 states, matched
5382 transitions (= visited+matched)
3 atomic steps
hash conflicts: 4 (resolved)

Stats on memory usage (in Megabytes):
0.271 equivalent memory usage for states (stored*(State-vector + overhead))
0.459 actual memory usage for states (unsuccessful compression: 169.54%)
state-vector as stored = 174 byte + 16 byte overhead
2.000 memory used for hash table (-w19)
0.305 memory used for DFS stack (-m10000)
2.696 total actual memory usage

unreached in proctype updatetimers
line 31, "pan.___", state 4, "timer = 0"
line 32, "pan.___", state 5, "avdelay = -(1)"
line 32, "pan.___", state 6, "lastpulse = 0"
line 36, "pan.___", state 12, "timer = 0"
line 37, "pan.___", state 13, "avdelay = -(1)"
line 37, "pan.___", state 14, "lastpacedpulsev = 0"
line 38, "pan.___", state 15, "lastpulse = 0"
line 42, "pan.___", state 21, "avdelay = -(1)"
line 43, "pan.___", state 22, "lastpacedpulsev = 0"
line 57, "pan.___", state 47, "-end-"
(10 of 47 states)
unreached in proctype environment
line 68, "pan.___", state 5, "lastpulse = timer"
line 68, "pan.___", state 6, "avdelay = 0"
line 68, "pan.___", state 8, "lastpulse = timer"
line 68, "pan.___", state 9, "avdelay = 0"
line 68, "pan.___", state 10, "pula = 1"
line 68, "pan.___", state 10, "timer = 0"
line 71, "pan.___", state 14, "avdelay = -(1)"
line 71, "pan.___", state 16, "avdelay = -(1)"
line 71, "pan.___", state 17, "pulv = 1"
line 71, "pan.___", state 17, "timer = 0"
line 82, "pan.___", state 30, "lastpulse = timer"
line 82, "pan.___", state 31, "avdelay = 0"
line 82, "pan.___", state 32, "pula = 1"
line 86, "pan.___", state 36, "avdelay = -(1)"
line 86, "pan.___", state 37, "timer = 0"
line 111, "pan.___", state 73, "-end-"
(14 of 73 states)
unreached in proctype sensor
line 119, "pan.___", state 10, "senv = 1"
line 119, "pan.___", state 11, "pulv = 0"
line 123, "pan.___", state 23, "-end-"
(3 of 23 states)
unreached in proctype pacegen
line 133, "pan.___", state 5, "lastpacedpulsev = timer"
line 133, "pan.___", state 6, "avdelay = -(1)"
line 133, "pan.___", state 7, "pulv = 1"
line 143, "pan.___", state 20, "lastpacedpulsea = timer"
line 143, "pan.___", state 21, "avdelay = 0"
line 143, "pan.___", state 22, "pula = 1"
line 152, "pan.___", state 34, "pulv = 1"
line 152, "pan.___", state 35, "lastpacedpulsev = timer"
line 152, "pan.___", state 36, "avdelay = -(1)"
line 160, "pan.___", state 47, "lastpacedpulsev = timer"
line 160, "pan.___", state 48, "avdelay = -(1)"
line 165, "pan.___", state 55, "lastpacedpulsev = timer"
line 165, "pan.___", state 56, "avdelay = -(1)"
line 165, "pan.___", state 57, "pulv = 1"
line 173, "pan.___", state 69, "lastpacedpulsea = timer"
line 173, "pan.___", state 70, "avdelay = 0"
line 178, "pan.___", state 77, "lastpacedpulsea = timer"
line 178, "pan.___", state 78, "avdelay = 0"
line 178, "pan.___", state 79, "pula = 1"
line 186, "pan.___", state 91, "pulv = 1"
line 186, "pan.___", state 92, "lastpacedpulsev = timer"
line 186, "pan.___", state 93, "avdelay = -(1)"
line 191, "pan.___", state 100, "lastpacedpulsev = timer"
line 191, "pan.___", state 101, "avdelay = -(1)"
line 191, "pan.___", state 102, "pulv = 1"
line 212, "pan.___", state 137, "avdelay = 0"
line 212, "pan.___", state 138, "sensea?_"
line 216, "pan.___", state 142, "lastpacedpulsev = timer"
line 216, "pan.___", state 143, "avdelay = -(1)"
line 216, "pan.___", state 144, "sensev?_"
line 218, "pan.___", state 147, "lastpacedpulsev = timer"
line 218, "pan.___", state 148, "avdelay = -(1)"
line 218, "pan.___", state 149, "pulsev!1"
line 226, "pan.___", state 166, "-end-"
(34 of 166 states)
unreached in proctype :init:
(0 of 6 states)
unreached in proctype :never:
line 298, "pan.___", state 11, "-end-"
(1 of 11 states)

pan: elapsed time 0.04 seconds
pan: rate 87100 states/second
pan: avg transition delay 7.4322e-06 usec
0.00user 0.02system 0:00.05elapsed 40%CPU (0avgtext+0avgdata 12928maxresident)k
0inputs+16outputs (0major+848minor)pagefaults 0swaps

#endif
159 changes: 159 additions & 0 deletions verified_pacemaker/AAI_H.ltl
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,159 @@
#define p sena == 1
#define q pula == 0
#define r avdelay == 0
#define s lastpacedpulsea == timer
#define t responsefactor == 10


/*
* Formula As Typed: [] (p -> <> (q && r && s && t))
* The Never Claim Below Corresponds
* To The Negated Formula !([] (p -> <> (q && r && s && t)))
* (formalizing violations of the original)
*/

never { /* !([] (p -> <> (q && r && s && t))) */
T0_init:
if
:: (((! ((q)) && (p)) || (((! ((r)) && (p)) || (((! ((s)) && (p)) || (! ((t)) && (p)))))))) -> goto accept_S3
:: (1) -> goto T0_init
fi;
accept_S3:
if
:: (((! ((q))) || (((! ((r))) || (((! ((s))) || (! ((t))))))))) -> goto accept_S3
fi;
}

#ifdef NOTES
Use Load to open a file or a template.







#endif
#ifdef RESULT
warning: for p.o. reduction to be valid the never claim must be stutter-invariant
(never claims generated from LTL formulae are stutter-invariant)
depth 0: Claim reached state 5 (line 385)
depth 1664: Claim reached state 9 (line 390)
depth 1726: Claim reached state 9 (line 390)

(Spin Version 5.2.5 -- 17 April 2010)
+ Partial Order Reduction

Full statespace search for:
never claim +
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)

State-vector 116 byte, depth reached 12407, errors: 0
31876 states, stored (46543 visited)
17465 states, matched
64008 transitions (= visited+matched)
4 atomic steps
hash conflicts: 375 (resolved)

Stats on memory usage (in Megabytes):
4.013 equivalent memory usage for states (stored*(State-vector + overhead))
3.377 actual memory usage for states (compression: 84.17%)
state-vector as stored = 95 byte + 16 byte overhead
2.000 memory used for hash table (-w19)
3.052 memory used for DFS stack (-m100000)
8.372 total actual memory usage

unreached in proctype updatetimers
line 45, "pan.___", state 12, "timer = 0"
line 46, "pan.___", state 13, "avdelay = -(1)"
line 46, "pan.___", state 14, "lastpacedpulsev = 0"
line 47, "pan.___", state 15, "lastpulse = 0"
line 51, "pan.___", state 21, "avdelay = -(1)"
line 52, "pan.___", state 22, "lastpacedpulsev = 0"
line 66, "pan.___", state 47, "-end-"
(7 of 47 states)
unreached in proctype environment
line 94, "pan.___", state 34, "lastpulse = timer"
line 94, "pan.___", state 35, "avdelay = 0"
line 94, "pan.___", state 36, "pula = 1"
line 98, "pan.___", state 40, "avdelay = -(1)"
line 98, "pan.___", state 41, "timer = 0"
line 110, "pan.___", state 54, "lastpulse = timer"
line 110, "pan.___", state 55, "avdelay = 0"
line 110, "pan.___", state 56, "timer = 0"
line 114, "pan.___", state 60, "avdelay = -(1)"
line 114, "pan.___", state 61, "timer = 0"
line 122, "pan.___", state 78, "-end-"
(11 of 78 states)
unreached in proctype sensor
line 133, "pan.___", state 19, "senv = 0"
line 133, "pan.___", state 20, "pulv = 0"
line 140, "pan.___", state 41, "-end-"
(3 of 41 states)
unreached in proctype pacegen
line 152, "pan.___", state 6, "pulv = 1"
line 152, "pan.___", state 7, "lastpacedpulsev = timer"
line 152, "pan.___", state 8, "avdelay = -(1)"
line 154, "pan.___", state 14, "pulv = 1"
line 154, "pan.___", state 15, "lastpacedpulsev = timer"
line 154, "pan.___", state 16, "avdelay = -(1)"
line 150, "pan.___", state 17, "(((((mode==VOOR)||(mode==DOOR))||(mode==DDDR))||(mode==VDDR)))"
line 150, "pan.___", state 17, "else"
line 166, "pan.___", state 31, "pula = 1"
line 166, "pan.___", state 32, "lastpacedpulsea = timer"
line 166, "pan.___", state 33, "avdelay = 0"
line 168, "pan.___", state 39, "pula = 1"
line 168, "pan.___", state 40, "lastpacedpulsea = timer"
line 168, "pan.___", state 41, "avdelay = 0"
line 164, "pan.___", state 42, "((((mode==AOOR)||(mode==DOOR))||(mode==DDDR)))"
line 164, "pan.___", state 42, "else"
line 176, "pan.___", state 54, "lastpacedpulsev = timer"
line 176, "pan.___", state 55, "avdelay = -(1)"
line 177, "pan.___", state 57, "responsefactor = 10"
line 186, "pan.___", state 69, "pulv = 1"
line 186, "pan.___", state 70, "lastpacedpulsev = timer"
line 186, "pan.___", state 71, "avdelay = -(1)"
line 188, "pan.___", state 77, "pulv = 1"
line 188, "pan.___", state 78, "lastpacedpulsev = timer"
line 188, "pan.___", state 79, "avdelay = -(1)"
line 184, "pan.___", state 80, "(((mode==VVIR)||(mode==DDIR)))"
line 184, "pan.___", state 80, "else"
line 206, "pan.___", state 107, "pula = 1"
line 206, "pan.___", state 108, "lastpacedpulsea = timer"
line 206, "pan.___", state 109, "avdelay = 0"
line 216, "pan.___", state 130, "pulv = 1"
line 216, "pan.___", state 131, "lastpacedpulsev = timer"
line 216, "pan.___", state 132, "avdelay = -(1)"
line 221, "pan.___", state 139, "lastpacedpulsev = timer"
line 221, "pan.___", state 140, "avdelay = -(1)"
line 221, "pan.___", state 141, "pulv = 1"
line 229, "pan.___", state 153, "pula = 1"
line 229, "pan.___", state 154, "lastpacedpulsea = timer"
line 229, "pan.___", state 155, "avdelay = 0"
line 234, "pan.___", state 162, "lastpacedpulsea = timer"
line 234, "pan.___", state 163, "avdelay = 0"
line 234, "pan.___", state 164, "pula = 1"
line 242, "pan.___", state 176, "avdelay = 0"
line 243, "pan.___", state 178, "responsefactor = 10"
line 248, "pan.___", state 188, "avdelay = -(1)"
line 255, "pan.___", state 199, "pulv = 1"
line 255, "pan.___", state 200, "lastpacedpulsev = timer"
line 255, "pan.___", state 201, "avdelay = -(1)"
line 262, "pan.___", state 217, "-end-"
(46 of 217 states)
unreached in proctype accelerometer
line 294, "pan.___", state 59, "-end-"
(1 of 59 states)
unreached in proctype :init:
(0 of 8 states)
unreached in proctype :never:
line 392, "pan.___", state 11, "-end-"
(1 of 11 states)

pan: elapsed time 0.783 seconds
pan: rate 59441.89 states/second
pan: avg transition delay 1.2233e-005 usec

#endif
Loading

0 comments on commit 7e91259

Please sign in to comment.