Newer
Older
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
Reachability Analysis:
1. Element start of block Wallet -> reachable
2. Element main of block Wallet -> reachable
3. Element action_on_signal__clone:getCoin of block Wallet -> reachable
4. Element start of block CoffeeMachine -> reachable
5. Element WaitingForFirstCoin of block CoffeeMachine -> reachable
6. Element action_on_signal__clone:getCoin of block CoffeeMachine -> reachable
7. Element WaitingForSecondCoin of block CoffeeMachine -> reachable
8. Element ejectState of block CoffeeMachine -> reachable
9. Element action_on_signal__clone:getCoin of block CoffeeMachine -> reachable
10. Element Beverage of block CoffeeMachine -> reachable
11. Element WaitingForSelection of block CoffeeMachine -> reachable
12. Element action_on_signal__clone:ejectCoin of block CoffeeMachine -> NOT reachable
13. Element action_on_signal__clone:pushCoffeeButton of block CoffeeMachine -> reachable
14. Element action_on_signal__clone:pushTeaButton of block CoffeeMachine -> reachable
15. Element start of block CoffeeButton -> reachable
16. Element main of block CoffeeButton -> reachable
17. Element state0 of block CoffeeButton -> reachable
18. Element start of block TeaButton -> reachable
19. Element main of block TeaButton -> reachable
Liveness Analysis:
1. Element start of block Wallet -> liveness is satisfied
2. Element main of block Wallet -> liveness is satisfied
3. Element action_on_signal__clone:getCoin of block Wallet -> liveness is NOT satisfied
4. Element start of block CoffeeMachine -> liveness is satisfied
5. Element WaitingForFirstCoin of block CoffeeMachine -> liveness is satisfied
6. Element action_on_signal__clone:getCoin of block CoffeeMachine -> liveness is satisfied
7. Element WaitingForSecondCoin of block CoffeeMachine -> liveness is satisfied
8. Element ejectState of block CoffeeMachine -> liveness is NOT satisfied
9. Element action_on_signal__clone:getCoin of block CoffeeMachine -> liveness is NOT satisfied
10. Element Beverage of block CoffeeMachine -> liveness is NOT satisfied
11. Element WaitingForSelection of block CoffeeMachine -> liveness is NOT satisfied
12. Element action_on_signal__clone:ejectCoin of block CoffeeMachine -> liveness is NOT satisfied
13. Element action_on_signal__clone:pushCoffeeButton of block CoffeeMachine -> liveness is NOT satisfied
14. Element action_on_signal__clone:pushTeaButton of block CoffeeMachine -> liveness is NOT satisfied
15. Element start of block CoffeeButton -> liveness is satisfied
16. Element main of block CoffeeButton -> liveness is satisfied
17. Element state0 of block CoffeeButton -> liveness is satisfied
18. Element start of block TeaButton -> liveness is satisfied
19. Element main of block TeaButton -> liveness is satisfied
All done. See you soon.