SHARE
TWEET

Untitled

a guest Apr 18th, 2019 74 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. byte g1 = 0;
  2. byte g2 = 0;
  3. byte g3 = 0;
  4. byte r1 = 0;
  5. byte r2 = 0;
  6. byte r3 = 0;
  7.  
  8. #define forallfrogs1(p) \
  9. :: p(g1) \
  10. :: p(g2) \
  11. :: p(g3) \
  12. :: p(r1) \
  13. :: p(r2) \
  14. :: p(r3)
  15.  
  16. #define forallfrogs2(p) \
  17. :: p(g1, r1) \
  18. :: p(g2, r2) \
  19. :: p(g3, r3) \
  20. :: p(r1, g1) \
  21. :: p(r2, g2) \
  22. :: p(r3, g3)
  23.  
  24. #define jumpon(x) (!(g1 == 1 || g2 == 1 || g3 == 1 || r1 == 1 || r2 == 1 || r3 == 1) && (x == 0)) -> x = 1
  25. #define jumpfromstone(x1, x2) ((x1 == 1) && (x2 == 2)) -> x1 = 2
  26. #define jumpacross(x1, x2) ((x2 == 1) && (x1 == 0)) -> x1 = 2
  27.  
  28. init {
  29.     do
  30.     forallfrogs1(jumpon)
  31.     forallfrogs2(jumpfromstone)
  32.     od
  33. }
  34.  
  35. ltl win {[]!(g1 == 2 && g2 == 2 && g3 == 2 && r1 == 2 && r2 == 2 && r3 == 2 ) }
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
 
Top