Skip to content
Snippets Groups Projects
Select Git revision
  • 1ab50739ade03d27749589c038b463773bae799c
  • master default protected
  • btypes-fixes
  • freetypes
  • embedded-codegen
  • rust-support
  • z3solver
7 results

QueensWithEvents_4.mch

Blame
  • Code owners
    Assign users and groups as approvers for specific file changes. Learn more.
    QueensWithEvents_4.mch 825 B
    /*
    From ProB examples
    */
    MACHINE QueensWithEvents_4
    // rewritten for B2Program by inlining DEFINITIONS
    // v2: rewrote perm(1..n) for B2Program
    CONSTANTS n
    PROPERTIES
     n : NATURAL &
     n = 4
    VARIABLES queens
    INVARIANT
      queens : 1..n +-> 1..n
    INITIALISATION
      queens := {}
    OPERATIONS
      Solve =
          ANY solution WHERE
            solution : POW((1..n) * (1..n))
          & solution : perm(1..n)
          &
            !(q1,q2).(
             (
              q1 : 1..n
              &
              q2 : (1..n) \ {1}
              &
              q2 > q1
             )
             =>
             (
              (solution(q1) + q2) - q1 /= solution(q2)
              &
              (solution(q1) - q2) + q1 /= solution(q2)
             )
            )
          &
            !x.(
             x : dom(queens)
             =>
             solution(x) = queens(x)
            )
      THEN
         queens := solution
      END
    
    END