%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                          Problem barber4-1 from the Action Language home page
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%
%	Note that comments begin with %
%

%
%	Here the problem name comes
%

problem barber4_1

%
%	All state variables must be declared, currently only
%	natural numbers-valued variables are supported
%
var
  barber : nat,
  chair : nat,
  open : nat,
  p1 : nat,
  p2 : nat,
  p3 : nat,
  p4 : nat,
  p5 : nat

%
%	Initial state. In formulas one can use 
%		& - conjunction
%		| - disjunction
%		~ - negation
%	as logical operators, and
%		=
%		!=
%		>
%		<
%		>=
%		<=
%	as comparison operators on integers
%
%
initial
  barber = 0 & chair = 0 & open = 0 &
  p1 = 0 & p2 = 0 & p3 = 0 & p4 = 0 & p5 = 0

%
%	Final state. We check reachability of a final state
%	from an initial state
%

final
  chair > 1

%
%  Try this reachable final state to see how the BRAIN shows the trace
%
%  chair > 0
%

%
%	If you want to detect deadlocks, use
%	   deadlock
%	instead of specificition of final states.
%
%	Try it to see an example for which the Brain diverges
%
%	For the deadlock I suggest to use
%   brain -i barberm4-1.br -s 1000000
%

%
%	Transitions in the form of guarded assignments, currently the
%	only supported form of transitions. Note that the variables
%	which are not assigned to preserve their values
%

transition t1
  p1 = 0 & barber > 0
    ->
        barber := barber-1,
        chair := chair+1,
        p1 := 1

transition t2
  p1 = 1 & open > 0
    ->
        open := open-1,
        p1 := 0

transition t3
  p2 = 0 & barber > 0
    ->
        barber := barber-1,
        chair := chair+1,
        p2 := 1

transition t4
  p2 = 1 & open > 0
    ->
        open := open-1,
        p2 := 0

transition t5
  p3 = 0 & barber > 0
    ->
        barber := barber-1,
        chair := chair+1,
        p3 := 1

transition t6
  p3 = 1 & open > 0
    ->
        open := open-1,
        p3 := 0

transition t7
  p4 = 0 & barber > 0
    ->
        barber := barber-1,
        chair := chair+1,
        p4 := 1

transition t8
  p4 = 1 & open > 0
    ->
        open := open-1,
        p4 := 0

transition t9
  p5 = 0
    ->
        barber := barber+1,
        p5 := 1

transition t10
  p5 = 1 & chair > 0
    ->
        chair := chair-1,
        p5 := 2

transition t11
  p5 = 2
    ->
        open := open+1,
        p5 := 3

transition t12
  p5 = 3 & open = 0
    ->
        p5 := 0


%
%	To run the BRAIN use
%	   brain -i <input-file>
%	One can also use 
%	   brain -i <input-file> -s <C>
%	For the latter form the BRAIN will output statistics
%	   after each C entailment checks
%