V.4 Tempura

Tempura [Slide 152]

• Would it not be nice to have a tool that would generate the interval corresponding to a given ITL formula?
• There exists such a tool: Tempura

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?