Android_Projects/PowerWindowSimulation.smv at master · ak9847/Android_Projects · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
-- Power window simulation demonstration using NUSMV
-- Assumptions
-- 1. Every second the window moves 2 frames hence the total length of the window is covered in 2 frames.


MODULE main
VAR
postion: 0 .. 10;
obstacle : boolean;
passengerButtonUp : boolean;
passengerButtonDown : boolean;
driverUp: boolean ;
driverDown: boolean;
continuouspressUp : boolean;
continuouspressDown : boolean;
passengerContinousUp : boolean;
passengerContinousDown : boolean ;


ASSIGN
init(postion) :=0;
init(continuouspressDown):= FALSE;
init(continuouspressUp) :=FALSE;
init(passengerContinousDown) :=FALSE;
init(passengerContinousUp) :=FALSE;

TRANS
case
-- considering all the cases with obstacles as obstacles has higher priority

(obstacle & driverUp) & (postion != 0) : next(postion) = postion - 2 ;

obstacle & driverDown : next(postion) = postion + 0  ;

(obstacle & passengerButtonUp) & (postion != 0) : next(postion)= postion - 2  ;
--
obstacle & passengerButtonDown : next(postion) = postion + 0 ;


-- considering all the cases with driver side as priority

-- implementing the continous press

driverUp & next(driverUp) & (postion != 10) : (next(postion) = postion + 2 )  & (next(continuouspressUp) = TRUE) ;

continuouspressUp & (postion != 10) : (next(postion) = postion + 2);

driverUp & (postion != 10) : next(postion) = postion + 2;


driverDown & next(driverDown) : next(postion) = postion - 2 & next(continuouspressDown) = TRUE ;

continuouspressDown : next(postion) = postion -2  ;

--
driverDown  & (postion != 0): next(postion) = postion - 2;


--considering all the cases with passenger side


passengerButtonUp & next(passengerButtonUp) & (postion != 10): (next(postion) = postion + 2) & (next(passengerContinousUp) = TRUE);

passengerContinousUp : (next(postion) = postion + 2) ;

passengerButtonUp  & (postion != 10) : next(postion) = postion + 2 ;

passengerButtonDown & next(passengerButtonDown) : (next(postion) = postion - 2) & (next(passengerContinousDown) = TRUE);

passengerContinousDown  : next(postion) = postion - 2 ;

passengerButtonDown  & (postion != 0) : next(postion) = postion - 2 ;

TRUE: next(postion) = postion + 0;
esac;


-- LTLSPEC

LTLSPEC F((!obstacle & (passengerButtonUp | driverUp)) -> postion = 2);

LTLSPEC G ((!obstacle & driverUp & continuouspressUp) -> (postion != 10));

LTLSPEC F(obstacle & (driverUp  | passengerButtonUp) -> postion = 10);

LTLSPEC F(!obstacle -> (postion = 10 | postion = 0));

LTLSPEC F(!obstacle & driverUp -> postion = 12);

LTLSPEC X(!obstacle & driverDown & passengerButtonUp -> postion = 2);