/***************************************************************************
*
* Copyright (c) 1989 -- 2000
* by Helsinki University of Technology, Digital Systems Laboratory.
* All rights reserved.
*
* Author of dekker.net: Kimmo Varpaaniemi
*
* Current version:
*     $Id$
*
* Description:
*     This model of Dekker's solution to the critical section problem
*     is used in an on-the-fly verification example in PROD Reference
*     Manual.
*
* Version history:
*     $Log$
***************************************************************************/

#place noncritical lo(<.1.>) hi(<.2.>) mk(<.1..2.>)
#place wait_set_b_i lo(<.1.>) hi(<.2.>)
#place wait_read_b_j lo(<.1.>) hi(<.2.>)
#place wait_read_k lo(<.1.>) hi(<.2.>)
#place wait_clear_b_i lo(<.1.>) hi(<.2.>)
#place wait_read_k_again lo(<.1.>) hi(<.2.>)
#place wait_set_b_i_again lo(<.1.>) hi(<.2.>)
#place wait_enter lo(<.1.>) hi(<.2.>)
#place critical lo(<.1.>) hi(<.2.>)
#place wait_set_k lo(<.1.>) hi(<.2.>)
#place wait_clear_b_i_again lo(<.1.>) hi(<.2.>)
#place b lo(<.1, 0.>) hi(<.2, 1.>) mk(<.1..2, 0.>)
#place k lo(<.1.>) hi(<.2.>) mk(<.1.>)
#place scheduler lo(<.0.>) hi(<.2.>) mk(<.0.>)
#trans choose_i
    in  { scheduler: <.0.>; }
    out { scheduler: <.i.>; }
    comp { i = 1; Accept(); i = 2; Accept(); }
#endtr
#trans do_noncritical
    in  { noncritical: <.i.>; scheduler: <.i.>; }
    out { noncritical: <.i.>; scheduler: <.0.>; }
#endtr
#trans desire
    in  { noncritical: <.i.>; scheduler: <.i.>; }
    out { wait_set_b_i: <.i.>; scheduler: <.0.>; }
#endtr
#trans set_b_i
    in  { wait_set_b_i: <.i.>; b: <.i, 0.>; scheduler: <.i.>; }
    out { wait_read_b_j: <.i.>; b: <.i, 1.>; scheduler: <.0.>; }
#endtr
#trans read_b_j_true
    in  { wait_read_b_j: <.i.>; b: <.3 - i, 1.>; scheduler: <.i.>; }
    out { wait_read_k: <.i.>; b: <.3 - i, 1.>; scheduler: <.0.>; }
#endtr
#trans read_b_j_false
    in  { wait_read_b_j: <.i.>; b: <.3 - i, 0.>; scheduler: <.i.>; }
    out { wait_enter: <.i.>; b: <.3 - i, 0.>; scheduler: <.0.>; }
#endtr
#trans read_k_eq_j
    in  { wait_read_k: <.i.>; k: <.3 - i.>; scheduler: <.i.>; }
    out { wait_clear_b_i: <.i.>; k: <.3 - i.>; scheduler: <.0.>; }
#endtr
#trans read_k_ne_j
    in  { wait_read_k: <.i.>; k: <.i.>; scheduler: <.i.>; }
    out { wait_read_b_j: <.i.>; k: <.i.>; scheduler: <.0.>; }
#endtr
#trans clear_b_i
    in  { wait_clear_b_i: <.i.>; b: <.i, 1.>; scheduler: <.i.>; }
    out { wait_read_k_again: <.i.>; b: <.i, 0.>; scheduler: <.0.>; }
#endtr
#trans read_k_again_eq_j
    in  { wait_read_k_again: <.i.>; k: <.3 - i.>; scheduler: <.i.>; }
    out { wait_read_k_again: <.i.>; k: <.3 - i.>; scheduler: <.0.>; }
#endtr
#trans read_k_again_ne_j
    in  { wait_read_k_again: <.i.>; k: <.i.>; scheduler: <.i.>; }
    out { wait_set_b_i_again: <.i.>; k: <.i.>; scheduler: <.0.>; }
#endtr
#trans set_b_i_again
    in  { wait_set_b_i_again: <.i.>; b: <.i, 0.>; scheduler: <.i.>; }
    out { wait_read_b_j: <.i.>; b: <.i, 1.>; scheduler: <.0.>; }
#endtr
#trans enter
    in  { wait_enter: <.i.>; scheduler: <.i.>; }
    out { critical: <.i.>; scheduler: <.0.>; }
#endtr
#trans exit
    in  { critical: <.i.>; scheduler: <.i.>; }
    out { wait_set_k: <.i.>; scheduler: <.0.>; }
#endtr
#trans set_k
    in  { wait_set_k: <.i.>; k: <.z.>; scheduler: <.i.>; }
    out { wait_clear_b_i_again: <.i.>; k: <.3 - i.>; scheduler: <.0.>; }
#endtr
#trans clear_b_i_again
    in  { wait_clear_b_i_again: <.i.>; b: <.i, 1.>; scheduler: <.i.>; }
    out { noncritical: <.i.>; b: <.i, 0.>; scheduler: <.0.>; }
#endtr