-- fairness constraints to be added to the SMV code
-- (for 2 agent model)

FAIRNESS s._Self = _agent____1____ 
FAIRNESS s._Self = _agent____2____ 

-- specification to be added to the SMV code (cf. Winter2001 p.93)

-- a) no two agents have exclusive access to the same line simultaneously
--AG ( (!(State(agent_1, line_1) = exclusive
--        & State(agent_2, line_1)=exclusive))
--    & (!(State(agent_1, line_2) = exclusive
--        & State(agent_2, line_2)=exclusive)) )

SPEC
AG ( ( ! ( s.__CCState_____agent____1_______lines____1________ = _exclusive
        &  s.__CCState_____agent____2_______lines____1________ = _exclusive ))
    & ( ! (s.__CurPhase_____agent____1_______lines____2________ = _exclusive 
        &  s.__CurPhase_____agent____2_______lines____2________ = _exclusive )))


-- b) each request will eventually be acknowledged
-- AG (CurrPhase(agent_i, l) = wait -> AF (CurrPhase(agent_i, l) = ready) )

AG ( s.__CurPhase_____agent____1_______lines____1________ = _wait
  -> AF ( s.__CurPhase_____agent____1_______lines____1________ = _ready ))
&
AG ( s.__CurPhase_____agent____1_______lines____2________ = _wait
  -> AF ( s.__CurPhase_____agent____1_______lines____2________ = _ready ))
&
AG ( s.__CurPhase_____agent____2_______lines____1________ = _wait
  -> AF ( s.__CurPhase_____agent____2_______lines____1________ = _ready ))
&
AG ( s.__CurPhase_____agent____2_______lines____2________ = _wait
  -> AF ( s.__CurPhase_____agent____2_______lines____2________ = _ready ))


-- c) whenever an agent gets shared access to a line, 
--    the line's home will note it as a sharer
-- AG ( State(agent_i, l) = shared -> AX (Sharer(l, agent_i) = true)
--         | Sharer(l, agent_i) = true -> AX (State(agent_i, l) = shared))

AG (( s.__CCState_____agent____1_______lines____1________ = _shared 
       -> AX (s.__Sharer_____lines____1_______agent____1________ = TRUE ))
   | ( s.__Sharer_____lines____1_______agent____1________ = TRUE 
       -> AX ( s.__CCState_____agent____1_______lines____1________ = _shared )))
&
AG (( s.__CCState_____agent____2_______lines____1________ = _shared 
       -> AX (s.__Sharer_____lines____1_______agent____2________ = TRUE ))
   | ( s.__Sharer_____lines____1_______agent____2________ = TRUE 
       -> AX ( s.__CCState_____agent____2_______lines____1________ = _shared )))
&
AG (( s.__CCState_____agent____1_______lines____2________ = _shared 
       -> AX (s.__Sharer_____lines____2_______agent____1________ = TRUE ))
   | ( s.__Sharer_____lines____2_______agent____1________ = TRUE 
       -> AX ( s.__CCState_____agent____1_______lines____2________ = _shared )))
&
AG (( s.__CCState_____agent____2_______lines____2________ = _shared 
       -> AX (s.__Sharer_____lines____2_______agent____2________ = TRUE ))
   | ( s.__Sharer_____lines____2_______agent____2________ = TRUE 
       -> AX ( s.__CCState_____agent____2_______lines____2________ = _shared )))