CONST

 ArSize : 4;
 ArSize_1 : ArSize - 1; 
 ArSizeP1 : ArSize + 1;

TYPE

 indT : 0..ArSize_1;
 bloatedindT : -1..ArSize;
 
 dT  : 0..ArSize; 
 arT : Array[indT] of dT;

VAR

 ar : arT;
 
 done : boolean;
 status : boolean;
 
 verifymode : boolean;
 curind : indT;
 itemsought : dT;
 
 low : bloatedindT;
 high : bloatedindT;

STARTSTATE

 verifymode := false;
 done := false;
 status := false; -- false means not found and true means found
 
 curind := 0;
 itemsought := 0;
 
 For i:indT Do
  ar[i] := 0;
 End;

 put "Start state over";
 
ENDSTARTSTATE;

RULE "Rand create 1"
 !verifymode ==>
    curind := (curind+1) % ArSize;
    --put "cur ind is ";
    --put curind;
    --put "\n";
ENDRULE;

RULE "Rand create 1"
 !verifymode ==>
    itemsought := (itemsought+1) % ArSizeP1;
ENDRULE;

RULE "Rand Array Assign"
 !verifymode ==>
    ar[curind] := itemsought;
ENDRULE;

-- mu -b -c binsrch.m
-- make binsrch
-- binsrch -vbfs -b40 -tv -ndl -m200 -p4 -d binsrch-trace

-- tests fine
-- Invariant
--  !(ar[0] = 3 & ar[1] = 1 & ar[2] = 2 & ar[3] = 0)
-- ;

RULE "Switch"
  !verifymode
  &
  !(Exists i:indT Do
     Exists j:indT Do
       i<j & ar[i]>ar[j]
     Endexists
    Endexists) 
  ==>
    verifymode := true;
    low := 0;
    high := ArSize_1;
ENDRULE;  

--- now do the binary search -- possible to have any array and any itemsought now ---

RULE "Done with success"
  verifymode 
  & !done
  & 
    ar[ (low+high)/2 ] = itemsought ==>
       done := true;
       status := true;
ENDRULE;

RULE "Switch high ptr"
  verifymode 
  & !done
  &
    itemsought < ar[ (low+high)/2 ] ==>
      high := (low+high)/2 - 1;
ENDRULE;

RULE "Switch low ptr"
  verifymode 
  & !done
  &
    itemsought > ar[ (low+high)/2 ] ==>
      low := (low+high)/2 + 1;
ENDRULE;

RULE "Done with failure"
  verifymode 
  & !done
  & low > high ==>
       done := true;
       status := false; -- redundant, but let's do it
ENDRULE;

INVARIANT
  (done & status -> ar[ (low+high)/2 ] = itemsought)
  &
  (done & !status -> !(Exists i:indT Do  ar[i] = itemsought Endexists))
;

/*--

Script started on Tue Jan 11 09:23:08 2011
[ganesh@line-ganesh3 lc-vc]$ This program should be regarded as a DEBUGGING aid, not as a 
certifier of correctness.
Call with the -l flag or read the license file for terms
and conditions of use.
Run this program with "-h" for the list of options.

Bugs, questions, and comments should be directed to
"melatti@di.uniroma1.it".

CMurphi compiler last modified date: Dec 29 2010
Include files last modified date:    Feb 03 2010
==========================================================================

==========================================================================
Caching Murphi Release 5.4.4
Finite-state Concurrent System Verifier.

Caching Murphi Release 5.4.4 is based on various versions of Murphi.
Caching Murphi Release 5.4.4 :
Copyright (C) 2009-2012 by Sapienza University of Rome.
Murphi release 3.1 :
Copyright (C) 1992 - 1999 by the Board of Trustees of
Leland Stanford Junior University.

==========================================================================

Protocol: binsrch

Algorithm:
	Verification by depth first search.
	with symmetry algorithm 3 -- Heuristic Small Memory Normalization
	with permutation trial limit 10.

Memory usage:

	* The size of each state is 30 bits (rounded up to 4 bytes).
	* The memory allocated for the hash table and state queue is
	  209 Mbytes.
	  With states hash-compressed to 40 bits, the maximum size of
	  the state space is 38836153 states.
	   * Use option "-k" or "-m" to increase this, if necessary.
	* Capacity in queue for depth-first search: 3883615 states.
	   * Change the constant gPercentActiveStates in mu_prolog.inc
	     to increase this, if necessary.
Start state over
Progress Report:

	10000 states explored in 0.38s, with 17562 rules fired and 6252 states in the queue.

==========================================================================

Status:

	No error found.

State Space Explored:

	17568 states, 43268 rules fired in 0.40s.

Omission Probabilities (caused by Hash Compaction):

	Pr[even one omitted state]    <= 0.000000

Analysis of State Space:

	There are rules that are never fired.
	If you are running with symmetry, this may be why.  Otherwise,
	please run this program with "-pr" for the rules information.
[ganesh@line-ganesh3 lc-vc]$ [ganesh@line-ganesh3 lc-vc]$ exit

Script done on Tue Jan 11 09:23:27 2011


--

Script started on Tue Jan 11 09:23:33 2011
[ganesh@line-ganesh3 lc-vc]$ This program should be regarded as a DEBUGGING aid, not as a 
certifier of correctness.
Call with the -l flag or read the license file for terms
and conditions of use.
Run this program with "-h" for the list of options.

Bugs, questions, and comments should be directed to
"melatti@di.uniroma1.it".

CMurphi compiler last modified date: Dec 29 2010
Include files last modified date:    Feb 03 2010
==========================================================================

==========================================================================
Caching Murphi Release 5.4.4
Finite-state Concurrent System Verifier.

Caching Murphi Release 5.4.4 is based on various versions of Murphi.
Caching Murphi Release 5.4.4 :
Copyright (C) 2009-2012 by Sapienza University of Rome.
Murphi release 3.1 :
Copyright (C) 1992 - 1999 by the Board of Trustees of
Leland Stanford Junior University.

==========================================================================

Protocol: binsrch

Algorithm:
	Verification by breadth first search.
	with symmetry algorithm 3 -- Heuristic Small Memory Normalization
	with permutation trial limit 10.

Memory usage:

	* The size of each state is 30 bits (rounded up to 4 bytes).
	* The memory allocated for the hash table and state queue is
	  209 Mbytes.
	  With states hash-compressed to 40 bits, the maximum size of
	  the state space is 38836153 states.
	   * Use option "-k" or "-m" to increase this, if necessary.
	* Capacity in queue for breadth-first search: 3883615 states.
	   * Change the constant gPercentActiveStates in mu_prolog.inc
	     to increase this, if necessary.
Start state over
Progress Report:

	10000 states explored in 0.34s, with 19901 rules fired and 2509 states in the queue.

==========================================================================

Status:

	No error found.

State Space Explored:

	17568 states, 43268 rules fired in 0.36s.

Omission Probabilities (caused by Hash Compaction):

	Pr[even one omitted state]    <= 0.000000
	Pr[even one undetected error] <= 0.000000
	Diameter of reachability graph: 24

Analysis of State Space:

	There are rules that are never fired.
	If you are running with symmetry, this may be why.  Otherwise,
	please run this program with "-pr" for the rules information.
[ganesh@line-ganesh3 lc-vc]$ [ganesh@line-ganesh3 lc-vc]$ exit

Script done on Tue Jan 11 09:23:42 2011

*/