Banking1.acts 8.4 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123
  1. [System]
  2. ss
  3. [Parameter]
  4. p1 (enum): v1, v2, v3
  5. p2 (enum): v1, v2, v3, v4
  6. p3 (enum): v1, v2, v3
  7. p4 (enum): v1, v2, v3
  8. p5 (enum): v1, v2, v3
  9. [Constraint]
  10. C1: (p5 != "v1" || p2 != "v4" || p3 != "v2" || p4 != "v3" || p1 != "v1")
  11. C2: (p1 != "v3" || p5 != "v2" || p4 != "v3" || p3 != "v1" || p2 != "v3")
  12. C3: (p1 != "v3" || p5 != "v1" || p4 != "v1" || p3 != "v2" || p2 != "v1")
  13. C4: (p5 != "v1" || p4 != "v1" || p3 != "v3" || p1 != "v1" || p2 != "v2")
  14. C5: (p1 != "v3" || p5 != "v1" || p4 != "v1" || p3 != "v2" || p2 != "v3")
  15. C6: (p1 != "v3" || p5 != "v1" || p3 != "v3" || p2 != "v4" || p4 != "v2")
  16. C7: (p5 != "v2" || p4 != "v3" || p3 != "v1" || p2 != "v3" || p1 != "v1")
  17. C8: (p4 != "v2" || p3 != "v1" || p2 != "v3" || p5 != "v3" || p1 != "v1")
  18. C9: (p1 != "v3" || p5 != "v2" || p4 != "v1" || p2 != "v4" || p3 != "v1")
  19. C10: (p5 != "v1" || p1 != "v2" || p2 != "v4" || p4 != "v3" || p3 != "v1")
  20. C11: (p5 != "v1" || p2 != "v4" || p4 != "v2" || p3 != "v1" || p1 != "v1")
  21. C12: (p1 != "v3" || p5 != "v1" || p2 != "v4" || p3 != "v2" || p4 != "v3")
  22. C13: (p3 != "v3" || p1 != "v2" || p4 != "v3" || p2 != "v1" || p5 != "v3")
  23. C14: (p1 != "v3" || p5 != "v2" || p4 != "v1" || p3 != "v1" || p2 != "v3")
  24. C15: (p5 != "v1" || p4 != "v1" || p3 != "v3" || p1 != "v2" || p2 != "v1")
  25. C16: (p1 != "v3" || p5 != "v2" || p2 != "v4" || p4 != "v3" || p3 != "v1")
  26. C17: (p5 != "v1" || p4 != "v1" || p3 != "v3" || p1 != "v2" || p2 != "v3")
  27. C18: (p1 != "v3" || p5 != "v1" || p4 != "v1" || p3 != "v3" || p2 != "v2")
  28. C19: (p5 != "v1" || p1 != "v2" || p4 != "v3" || p2 != "v1" || p3 != "v1")
  29. C20: (p5 != "v1" || p4 != "v1" || p3 != "v3" || p1 != "v2" || p2 != "v4")
  30. C21: (p4 != "v1" || p3 != "v3" || p5 != "v3" || p1 != "v1" || p2 != "v2")
  31. C22: (p5 != "v1" || p4 != "v1" || p2 != "v4" || p3 != "v2" || p1 != "v1")
  32. C23: (p1 != "v3" || p2 != "v4" || p3 != "v2" || p4 != "v3" || p5 != "v3")
  33. C24: (p5 != "v1" || p4 != "v1" || p1 != "v2" || p3 != "v1" || p2 != "v3")
  34. C25: (p1 != "v3" || p4 != "v1" || p3 != "v2" || p2 != "v3" || p5 != "v3")
  35. C26: (p5 != "v1" || p4 != "v1" || p3 != "v1" || p1 != "v1" || p2 != "v2")
  36. C27: (p1 != "v3" || p2 != "v4" || p4 != "v2" || p3 != "v1" || p5 != "v3")
  37. C28: (p1 != "v3" || p3 != "v3" || p4 != "v2" || p2 != "v1" || p5 != "v3")
  38. C29: (p5 != "v1" || p3 != "v3" || p1 != "v2" || p4 != "v3" || p2 != "v1")
  39. C30: (p5 != "v1" || p3 != "v3" || p4 != "v2" || p2 != "v3" || p1 != "v1")
  40. C31: (p5 != "v1" || p3 != "v3" || p1 != "v2" || p4 != "v3" || p2 != "v3")
  41. C32: (p5 != "v2" || p3 != "v3" || p2 != "v4" || p4 != "v3" || p1 != "v1")
  42. C33: (p1 != "v3" || p5 != "v1" || p3 != "v2" || p4 != "v3" || p2 != "v3")
  43. C34: (p4 != "v1" || p1 != "v2" || p2 != "v4" || p3 != "v1" || p5 != "v3")
  44. C35: (p1 != "v3" || p5 != "v1" || p3 != "v2" || p4 != "v3" || p2 != "v1")
  45. C36: (p1 != "v3" || p5 != "v2" || p4 != "v1" || p3 != "v3" || p2 != "v1")
  46. C37: (p1 != "v2" || p2 != "v4" || p4 != "v3" || p3 != "v1" || p5 != "v3")
  47. C38: (p1 != "v3" || p5 != "v2" || p4 != "v1" || p3 != "v3" || p2 != "v3")
  48. C39: (p1 != "v3" || p5 != "v2" || p4 != "v1" || p3 != "v3" || p2 != "v4")
  49. C40: (p1 != "v3" || p5 != "v1" || p4 != "v1" || p3 != "v1" || p2 != "v2")
  50. C41: (p1 != "v3" || p5 != "v2" || p3 != "v3" || p2 != "v4" || p4 != "v3")
  51. C42: (p1 != "v3" || p5 != "v1" || p4 != "v2" || p3 != "v1" || p2 != "v3")
  52. C43: (p5 != "v2" || p4 != "v1" || p3 != "v3" || p2 != "v1" || p1 != "v1")
  53. C44: (p1 != "v3" || p5 != "v1" || p4 != "v3" || p3 != "v1" || p2 != "v2")
  54. C45: (p1 != "v3" || p5 != "v1" || p2 != "v4" || p4 != "v2" || p3 != "v1")
  55. C46: (p1 != "v2" || p4 != "v3" || p2 != "v1" || p3 != "v1" || p5 != "v3")
  56. C47: (p4 != "v3" || p3 != "v1" || p5 != "v3" || p1 != "v1" || p2 != "v2")
  57. C48: (p5 != "v1" || p4 != "v1" || p1 != "v2" || p2 != "v1" || p3 != "v1")
  58. C49: (p3 != "v3" || p2 != "v4" || p4 != "v2" || p5 != "v3" || p1 != "v1")
  59. C50: (p5 != "v1" || p3 != "v3" || p2 != "v4" || p4 != "v2" || p1 != "v1")
  60. C51: (p1 != "v3" || p5 != "v1" || p4 != "v2" || p2 != "v1" || p3 != "v1")
  61. C52: (p1 != "v3" || p4 != "v1" || p3 != "v2" || p2 != "v1" || p5 != "v3")
  62. C53: (p1 != "v3" || p3 != "v3" || p4 != "v3" || p5 != "v3" || p2 != "v2")
  63. C54: (p1 != "v3" || p3 != "v2" || p4 != "v3" || p2 != "v1" || p5 != "v3")
  64. C55: (p4 != "v1" || p3 != "v3" || p1 != "v2" || p2 != "v4" || p5 != "v3")
  65. C56: (p5 != "v1" || p3 != "v3" || p4 != "v2" || p2 != "v1" || p1 != "v1")
  66. C57: (p1 != "v3" || p5 != "v1" || p4 != "v1" || p2 != "v4" || p3 != "v2")
  67. C58: (p1 != "v3" || p4 != "v1" || p2 != "v4" || p3 != "v2" || p5 != "v3")
  68. C59: (p4 != "v1" || p1 != "v2" || p3 != "v1" || p2 != "v3" || p5 != "v3")
  69. C60: (p5 != "v1" || p3 != "v2" || p4 != "v3" || p2 != "v1" || p1 != "v1")
  70. C61: (p5 != "v2" || p4 != "v1" || p3 != "v3" || p2 != "v3" || p1 != "v1")
  71. C62: (p4 != "v2" || p2 != "v1" || p3 != "v1" || p5 != "v3" || p1 != "v1")
  72. C63: (p5 != "v2" || p4 != "v1" || p2 != "v1" || p3 != "v1" || p1 != "v1")
  73. C64: (p5 != "v1" || p4 != "v2" || p3 != "v1" || p2 != "v3" || p1 != "v1")
  74. C65: (p4 != "v1" || p2 != "v4" || p3 != "v2" || p5 != "v3" || p1 != "v1")
  75. C66: (p1 != "v3" || p4 != "v1" || p3 != "v3" || p5 != "v3" || p2 != "v2")
  76. C67: (p1 != "v3" || p4 != "v1" || p3 != "v1" || p5 != "v3" || p2 != "v2")
  77. C68: (p4 != "v1" || p1 != "v2" || p2 != "v1" || p3 != "v1" || p5 != "v3")
  78. C69: (p4 != "v1" || p3 != "v3" || p1 != "v2" || p2 != "v3" || p5 != "v3")
  79. C70: (p1 != "v3" || p5 != "v2" || p4 != "v1" || p2 != "v1" || p3 != "v1")
  80. C71: (p5 != "v1" || p4 != "v2" || p2 != "v1" || p3 != "v1" || p1 != "v1")
  81. C72: (p5 != "v2" || p4 != "v1" || p3 != "v1" || p2 != "v3" || p1 != "v1")
  82. C73: (p4 != "v1" || p3 != "v1" || p5 != "v3" || p1 != "v1" || p2 != "v2")
  83. C74: (p5 != "v2" || p4 != "v1" || p2 != "v4" || p3 != "v1" || p1 != "v1")
  84. C75: (p5 != "v1" || p4 != "v1" || p3 != "v2" || p2 != "v3" || p1 != "v1")
  85. C76: (p1 != "v3" || p5 != "v1" || p3 != "v3" || p4 != "v2" || p2 != "v3")
  86. C77: (p1 != "v3" || p4 != "v3" || p3 != "v1" || p5 != "v3" || p2 != "v2")
  87. C78: (p1 != "v3" || p5 != "v1" || p3 != "v3" || p4 != "v2" || p2 != "v1")
  88. C79: (p5 != "v2" || p3 != "v3" || p4 != "v3" || p2 != "v3" || p1 != "v1")
  89. C80: (p1 != "v3" || p3 != "v3" || p4 != "v2" || p2 != "v3" || p5 != "v3")
  90. C81: (p1 != "v3" || p5 != "v2" || p4 != "v3" || p2 != "v1" || p3 != "v1")
  91. C82: (p1 != "v3" || p3 != "v2" || p4 != "v3" || p2 != "v3" || p5 != "v3")
  92. C83: (p1 != "v3" || p4 != "v2" || p3 != "v1" || p2 != "v3" || p5 != "v3")
  93. C84: (p5 != "v1" || p1 != "v2" || p4 != "v3" || p3 != "v1" || p2 != "v3")
  94. C85: (p3 != "v3" || p4 != "v2" || p2 != "v3" || p5 != "v3" || p1 != "v1")
  95. C86: (p5 != "v1" || p3 != "v3" || p1 != "v2" || p2 != "v4" || p4 != "v3")
  96. C87: (p4 != "v1" || p3 != "v2" || p2 != "v1" || p5 != "v3" || p1 != "v1")
  97. C88: (p5 != "v1" || p3 != "v2" || p4 != "v3" || p2 != "v3" || p1 != "v1")
  98. C89: (p2 != "v4" || p4 != "v2" || p3 != "v1" || p5 != "v3" || p1 != "v1")
  99. C90: (p1 != "v3" || p5 != "v2" || p3 != "v3" || p4 != "v3" || p2 != "v3")
  100. C91: (p5 != "v1" || p4 != "v1" || p1 != "v2" || p2 != "v4" || p3 != "v1")
  101. C92: (p3 != "v3" || p1 != "v2" || p4 != "v3" || p2 != "v3" || p5 != "v3")
  102. C93: (p1 != "v3" || p5 != "v2" || p3 != "v3" || p4 != "v3" || p2 != "v1")
  103. C94: (p1 != "v3" || p5 != "v1" || p3 != "v3" || p4 != "v3" || p2 != "v2")
  104. C95: (p4 != "v1" || p3 != "v3" || p1 != "v2" || p2 != "v1" || p5 != "v3")
  105. C96: (p2 != "v4" || p3 != "v2" || p4 != "v3" || p5 != "v3" || p1 != "v1")
  106. C97: (p4 != "v1" || p3 != "v2" || p2 != "v3" || p5 != "v3" || p1 != "v1")
  107. C98: (p3 != "v2" || p4 != "v3" || p2 != "v1" || p5 != "v3" || p1 != "v1")
  108. C99: (p3 != "v3" || p1 != "v2" || p2 != "v4" || p4 != "v3" || p5 != "v3")
  109. C100: (p1 != "v2" || p4 != "v3" || p3 != "v1" || p2 != "v3" || p5 != "v3")
  110. C101: (p5 != "v2" || p4 != "v3" || p2 != "v1" || p3 != "v1" || p1 != "v1")
  111. C102: (p1 != "v3" || p4 != "v2" || p2 != "v1" || p3 != "v1" || p5 != "v3")
  112. C103: (p3 != "v3" || p4 != "v3" || p5 != "v3" || p1 != "v1" || p2 != "v2")
  113. C104: (p5 != "v1" || p3 != "v3" || p4 != "v3" || p1 != "v1" || p2 != "v2")
  114. C105: (p3 != "v2" || p4 != "v3" || p2 != "v3" || p5 != "v3" || p1 != "v1")
  115. C106: (p5 != "v2" || p2 != "v4" || p4 != "v3" || p3 != "v1" || p1 != "v1")
  116. C107: (p1 != "v3" || p3 != "v3" || p2 != "v4" || p4 != "v2" || p5 != "v3")
  117. C108: (p5 != "v1" || p4 != "v3" || p3 != "v1" || p1 != "v1" || p2 != "v2")
  118. C109: (p5 != "v1" || p4 != "v1" || p3 != "v2" || p2 != "v1" || p1 != "v1")
  119. C110: (p5 != "v2" || p4 != "v1" || p3 != "v3" || p2 != "v4" || p1 != "v1")
  120. C111: (p3 != "v3" || p4 != "v2" || p2 != "v1" || p5 != "v3" || p1 != "v1")
  121. C112: (p5 != "v2" || p3 != "v3" || p4 != "v3" || p2 != "v1" || p1 != "v1")