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
  26. deadlock = 1 &
  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. OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!
 
Top