//Fast File Modified for ranking stuff - 2010, Apr 08,12:13:24 model determinant{ //parameters i__o, j__o, k__o, n__o; var i, j, k, n, i__o, j__o, k__o, n__o; states start, a, d, b, c, halt, ____start; transition t0 :={ from := start ; to := a ; guard := n>=1; action := ; }; transition t1 :={ from := a ; to := d ; guard := true; action := k' = 1; }; transition t2 :={ from := d ; to := b ; guard := k=n; action := i' = i; }; transition t4 :={ from := b ; to := d ; guard := i>n; action := k' = 1 + k; }; transition t5 :={ from := b ; to := c ; guard := i<=n; action := j' = n; }; transition t6 :={ from := c ; to := c ; guard := j>k; action := j' = j - 1; }; transition t7 :={ from := c ; to := b ; guard := j<=k; action := i' = 1 + i; }; transition ____inittransition :={ from := ____start ; to := start ; guard := true; action := i' = i__o,j' = j__o,k' = k__o,n' = n__o; }; } strategy xx { Region init:={ state = ____start && true}; } // Result of Analysis //invariant start := n=n__o && k=k__o && j=j__o && i=i__o ; //invariant a := n>=1 && i=i__o && j=j__o && k=k__o && n=n__o ; //invariant d := k=1 && k>=1 && n=n__o ; //invariant b := i<=n+1 && k=1 && i>=k+1 && n=n__o ; //invariant c := j<=n && i<=n && k>=1 && j+1>k && i>=k+1 && n=n__o ; //invariant halt := n>=1 && k=n && n=n__o ; //invariant ____start := true ;