-- procedure bubblesort;
--  var j, t: integer;
--  begin
--  repeat
--    t:=a[1];
--    for j:=2 to N do
--      if a[j-1]>a[j] then
--      begin t:=a[j-1]; a[j-1]:=a[j]; a[j]:=t end
--  until t=a[1];
--  end;
--

CONST
 indMax   : 4;
 indMaxP1 : indMax+1;
 
 indMin   : 1;
 indMin_1 : indMin-1;

 dMin : 0;
 dMax : 2;

TYPE
 sT : ENUM {S0, S1, S2, S3};
 indRangeT  : indMin..indMax;
 drangeT    : dMin..dMax;
 
 arT        : Array [indRangeT] of drangeT;

VAR
 temp_ind : indMin_1 .. indMaxP1;
 temp_dat : drangeT;
 fillmode : boolean;
 ar : arT;
 state : sT;

STARTSTATE
 --
 state := S0;
 --
 fillmode := true;
 --
 temp_ind := indMin;
 temp_dat := dMin;
 --
 For i:indRangeT Do
  ar[i] := 0;
 End;
 --
 put "Start state over";
ENDSTARTSTATE;


RULE "Rand poise 1"
 fillmode ==> if temp_ind > indMin then temp_ind := temp_ind - 1 endif;
ENDRULE;

RULE "Rand poise 2"
 fillmode ==> if temp_ind < indMax then temp_ind := temp_ind + 1 endif;
ENDRULE;

RULE "Rand data 1"
 fillmode ==> if temp_dat > dMin then temp_dat := temp_dat - 1 endif;
ENDRULE;

RULE "Rand data 2"
 fillmode ==> if temp_dat < dMax then temp_dat := temp_dat + 1 endif;
ENDRULE;

RULE "fill"
 fillmode ==> ar[temp_ind] := temp_dat;
ENDRULE;

RULE "switch"
 fillmode ==> fillmode := false;
ENDRULE;

-->1 passed
-->1 INVARIANT
-->1 !(ar[1]=2 & ar[2]=0 & ar[3]=1 & ar[4]=0)
-->1 ;


RULE "working phase 1"
 !fillmode & state=S0 ==>
    temp_dat := ar[aMinIndx];
    temp_ind := indMin+1;
    state := S1;
ENDRULE;

RULE "working phase 2"
 !fillmode & state=S1 & temp_ind > indMax
  ==> state := S2;
ENDRULE;

RULE "working phase 3"
 !fillmode & state=S1 & temp_ind <= indMax & ar[temp_ind-1] > ar[temp_ind] 
  ==> temp_dat := ar[temp_ind-1];
      ar[temp_ind-1] := ar[temp_ind];
      ar[temp_ind] := temp_dat;
      UNDEFINE temp_dat;
      state := S2;
ENDRULE;