• API
• FAQ
• Tools
• Archive
SHARE
TWEET

# Untitled

a guest Jun 19th, 2019 79 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
1. MODULE main
2. VAR
3. e : { e1 , e2 , e3 , e4 , e5 , e6 , e7 , e8 , e9 , e10 , e11 , e12 } ;
4. j : 3..9;
5. i : 1..7;
6. x: 0..6;
7. primes : β 1..10;
8. factorial : 1..720;
9. sigma : 0 . . 1 0 ;
10. deadlock : 1 . . 3 ;
11. c : 0..10;
12. FROZENVAR number : 0 . . 8 ;
13. ββDEFINE number := 5 ;
14.
15. ASSIGN
16. i n i t ( e ) := e1 ;
17. i n i t ( j ) := 3 ;
18. i n i t ( i ) := 1 ;
19. i n i t ( p r i m e s ) := 0 ;
20. i n i t ( f a c t o r i a l ) := 1 ;
21. i n i t ( sigma ) := 0 ;
22. i n i t ( d e a d l o c k ) := 1 ;
23. i n i t ( c ) := 0 ;
24.
25. next ( deadlock ) := case
27. j = next ( j ) &
28. x = next ( x ) &
29. sigma = next ( sigma ) &
30. factorial = next ( factorial ) &
31. primes = next ( primes ) &
32. i = next ( i ) &
33. c = next ( c ) &
34. e = next ( e ) : 2 ;
35. deadlock = 2 : 3;
36. TRUE : d e a d l o c k ;
37. esac ;
38. n e x t ( e ) := c a s e
39. e = e1 & number > 2 : e2 ;
40. e = e1 & number <= 2 : e12 ;
41. e = e2 & j <= number : e3 ;
42. e = e2 & j > number : e8 ;
43. e = e3 : e4 ;
44. e = e4 & x < ( j β 2 ) : e5 ;
45. e = e4 & x >= ( j β 2 ) : e7 ;
46. e = e5 : e6 ;
47. e = e6 : e4 ;
48. e = e7 : e2 ;
49. e = e8 : e9 ;
50. e = e9 & number = 3 : e10 ;
51. e = e9 & number != 3 : e11 ;
52. TRUE : e;
53. esac ;
54.
55.
56. next ( x ) := c a s e
57. e = e3 & next ( e ) = e4 : 0 ;
58. e = e6 & next ( e ) = e4 & x + 1 <= 6 : x + 1 ;
59. TRUE : x ;
60. esac ;
61. next ( j ) := case
62. e = e7 & next ( e ) = e2 & j <= 8 : j + 1 ;
63. TRUE : j ;
64. esac ;
65.
66. next ( factorial ) := c a s e
67. e = e3 : 1 ;
68. next ( e ) = e5 & factorial <= 720 & factorial β i <= 720 : factorial β i ;
69. TRUE : factorial ;
70. esac ;
71. next ( i ) := case
72. next ( e ) = e3 : 1 ;
73. next ( e ) = e6 & i < 7 : i + 1 ;
74. TRUE : i ;
75. esac ;
76. next ( sigma ) := case
77. e = e7 & ( sigma + ( factorial β j β ( factorial / j ) ) ) <= 10 : sigma + ( factorial β j β (
78. factorial / j )) ;
79. TRUE : sigma ;
80. esac ;
81. next ( primes ) := case
82. e = e8 & (β1 + sigma ) >= 0 & (β1+sigma ) <= 10 : (β1 + sigma ) ;
83. TRUE : primes ;
84. esac ;
85.
86. next ( c ) := case
87. c + 1 > 10 : c ;
88. e = e3 : c + 1 ;
89. TRUE : c ;
90. esac ;
91.
92. CTLSPEC(number<3)-> AF e=e12;
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.
Not a member of Pastebin yet?