-
Notifications
You must be signed in to change notification settings - Fork 0
/
QA.txt
23 lines (18 loc) · 957 Bytes
/
QA.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
Combine req 6
true
%%%% 6a %%% %true
%%%% i %%%% %true
&& ([true* . getBatteryLevel(Empty)] mu X . ([!(conBatteryToMotor(0))] X && <true> true))
%%% ii %%%% %true
&& ([true* . getBatteryLevel(Empty)
. !(getBatteryLevel(Medium) || getBatteryLevel(Full))*]
(forall m : Nat . val(m > 0) => [conBatteryToMotor(m)] false))
%%%% 6b %%% %true
%%%% i %%%% %true
&& ([true* . getSolarPower(0)] mu X . ([!conSolarPanelToMotor(0)] X && <true> true))
&& ([true* . getSolarPower(0)] mu X . ([!conSolarPanelToBattery(0)] X && <true> true))
%%% ii %%%% %true
&& ([true* . getSolarPower(0)] [(forall n : Nat . val(n > 0) => !getSolarPower(n))*]
(forall m: Int . val(m > 0) => [conSolarPanelToMotor(m)] false))
&& ([true* . getSolarPower(0)] [(forall n : Nat . val(n > 0) => !getSolarPower(n))*]
(forall m: Int . val(m > 0) => [conSolarPanelToBattery(m)] false))