% System accepts two positive integers in variables x and y and
% places in variable z their integer quotient x div y, and in variable 
% w the remainder of their division x mod y.
% Prove the validity of the stated system invariant.

automaton IntegerDivision
  signature
    internal initialize, compute
    output halt
  states
    x : Int,
    y : Int,
    z : Int,
    w : Int,
    t : Int,
    init : Bool := true,
    done : Bool := false

  initially x > 0 /\ y > 0

  transitions
    internal initialize
      pre init
      eff t:= x;
	  z:= 0;
	  w:= 0;
          init := false

    internal compute
      pre ~init /\ ~done /\ t>0
      eff if w+1=y then z:=z+1 ; w := 0 else w := w+1 fi;
	  t := t-1

    output halt
      pre ~init /\ ~done /\ t <= 0
      eff done := true

invariant of IntegerDivision:
  done => x = (z*y) + w /\ 0 <= w /\ w < y