ZedPump/LineAlarmspec.zed at master · ZackC/ZedPump · 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
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
\documentclass{article}
\usepackage{czt}

\begin{document}
\begin{zsection}
  \SECTION LineAlarmspec \parents standard\_toolkit
\end{zsection}

This specification describes ...

This type represents the different states
of if the line is clear and
able to dispense if other conditions are
correct or blocked and not able to dispense
\begin{zed}
  ErrorState ::= clear | blocked % added this
\end{zed}

This type represents the different problems
possible in the line.  occlusion means the
line is plugged or pinched.  out_of_medicine
means that the line does not have
\begin{zed}
  Problem ::= occlusion | out\_of\_medicine
\end{zed}

This type represents the possible states of the
alarm for the line. If the alarm is sounding,
it means there exists a problem with the line.
If the alarm is silent then all is well.
\begin{zed}
  AlarmState ::= sounding | silent
\end{zed}


This schema represents the current amount of medicine
on a specific line. The invariants ensure that in all
cases where the line has a problem, the alarm is sounding
and in all cases where the line has no problems, the alarm
is silent.
\begin{schema}{MedicineLine}
  medicineAmount: \nat \\
  currentProblems : \power Problem\\
  alarm : AlarmState %added this
  \where
  currentProblems \neq \emptyset \implies alarm = sounding\\ %added this
  currentProblems = \emptyset \implies alarm = silent %added this
\end{schema}

The initial state of the medicine on a line is to be empty
\begin{schema}{InitMedicineLine}
  MedicineLine
\where
  medicineAmount = 0 \\
  currentProblems = \emptyset %added this
\end{schema}

Defines the amount of medicine put in the line
when it is filled up.
\begin{axdef}
  fillAmount: \nat
\where
  fillAmount = 2
\end{axdef}


The action modelling refilling the medicine in a line.
It can be done at any time and fills the medicine
back up to the fillAmount.
\begin{schema}{RefillLine}
  \Delta MedicineLine
\where
  medicineAmount' = fillAmount \\
  currentProblems' = currentProblems \setminus \{out\_of\_medicine\} %added this
\end{schema}

\begin{schema}{FixOcclusion} %added this
  \Delta MedicineLine
\where
  occlusion \in currentProblems\\
  currentProblems' = currentProblems \setminus \{occlusion\}\\
  medicineAmount' = medicineAmount
\end{schema}

The dispense medicince action dispenses one unit of
medicine per action.  It requires that the amount
of medicine in the line is greater than 0.
\begin{schema}{SuccessfulDispenseMedicine}
  \Delta MedicineLine
\where
  currentProblems = \emptyset\\
  medicineAmount > 0 \\
  medicineAmount' = medicineAmount - 1 \\ % added this
  currentProblems' = currentProblems
\end{schema}

This function models the medicine dispensing becoming
blocked.  The schema has the same pre states as the
SuccessfulDispenseMedicine schema
\begin{schema}{DispenseMedicineGetsBlocked} % added this
  \Delta MedicineLine
\where
  currentProblems = \emptyset\\
  medicineAmount > 0 \\
  medicineAmount' = medicineAmount \\ % added this
  currentProblems' = currentProblems \cup \{occlusion\}  % added this
\end{schema}


This function modles the line attempting to
dispense medicine while the line is out of
medicine.
\begin{schema}{AttemptDispenseWhenOutOfMedicine} % added this
  	\Delta MedicineLine
\where
  currentProblems = \emptyset\\
	medicineAmount = 0\\
	medicineAmount' = medicineAmount\\
	currentProblems' = currentProblems \cup \{out\_of\_medicine\}
\end{schema}

This schema prevents dispensing any medicine
when there is a problem.
\begin{schema}{AttemptDispenseWithProblem} % added this
  	\Xi MedicineLine
\where
  currentProblems \neq \emptyset\\
\end{schema}

This schema represents the ability of the line to become
blocked while dispensing but also allows the line to
dispense medicince successfully.
\begin{zed}
  NonDeterministicDispenseMedicine == SuccessfulDispenseMedicine \lor DispenseMedicineGetsBlocked % added this
\end{zed}

This schema represents all possible outcomes when trying to
dispense medicine under various conditions.
\begin{zed} %added this
  RDispenseMedicine == NonDeterministicDispenseMedicine \lor AttemptDispenseWhenOutOfMedicine \lor AttemptDispenseWithProblem
\end{zed}


\end{document}