define test() = { exists A: { halt(A=0) and A=8 and chopstar(skip and A:=A-2) and always output(A) } }.
Output:
State 0: A=8 State 1: A=6 State 2: A=4 State 3: A=2 State 4: A=0
A more complicated example:
/∗ run ∗/ define miracle() = exists A,I : { list (A, 12) and stable (struct (A)) and forall i < |A| : { A[i] = Random mod 20 } and I = 0 and always (output A) and chopstar { forall i < (|A| - 1) : { if I = i mod 2 then { if A[i] > A[i + 1] then (A[i] := A[i + 1] and A[i + 1] := A[i]) else (A[i] := A[i] and A[i + 1] := A[i + 1]) } } and
skip and I:=(I+1) mod 2 and if |A| mod 2 = 1 then { if I = 0 then A[|A|-1] := A[|A|-1] else A[0] := A[0] } else { if I = 1 then { if A[0] > A[|A|-1] then (A[0] := A[|A|-1] and A[|A|-1] := A[0]) else (A[0] := A[0] and A[|A|-1] := A[|A|-1]) } } } /∗ chopstar ∗/ and halt( forall i<(|A|-1) : A[i] <= A[i + 1]) }.
Output:
State 0: A=[10,15,3,4,10,18,16,4,4,13,11,5] State 1: A=[10,15,3,4,10,18,4,16,4,13,5,11] State 2: A=[10,3,15,4,10,4,18,4,16,5,13,11] State 3: A=[3,10,4,15,4,10,4,18,5,16,11,13] State 4: A=[3,4,10,4,15,4,10,5,18,11,16,13] State 5: A=[3,4,4,10,4,15,5,10,11,18,13,16] State 6: A=[3,4,4,4,10,5,15,10,11,13,18,16] State 7: A=[3,4,4,4,5,10,10,15,11,13,16,18] State 8: A=[3,4,4,4,5,10,10,11,15,13,16,18] State 9: A=[3,4,4,4,5,10,10,11,13,15,16,18]
So why is this “program” called miracle?