--- In (Balbiani, Herzig, Troquard, 2013 LICS) a supposedly polynomial
--- reduction from the problem PEEK-G5 (Stockemeyer Chandra 1979) into
--- the model checking problem in the logic of DL-PA is proposed. If
--- the reduction were actually working, a similar reduction could be
--- done from PEEK-G5 into the model checking problem of CTL over
--- NuSMV models.
--- We consider here the Peek instance where Eloise controls ep1, and
--- Abelard controls ap1 and ap2. Abelard plays first (Tau = A). The
--- goal formula Phi for this instance is ep1 & ap1. The valuation to
--- start with is empty: ep1, ap1, and ap2 are set to false. Clearly,
--- if Abelard never assigns true to ap1, Phi can never become
--- true. So clearly, Eloise does not have a winning strategy. So,
--- were the reduction working, we should not find a counter-model
--- when evaluating the present file. But a counter-model is found. So
--- the reduction in (Balbiani, Herzig, Troquard, 2013 LICS) is wrong.
MODULE abelard(turn, Phi)
--- Abelard controls two variables ap1 and ap2, both initially set to
--- false. Abelard can non-deterministically choose which variable to
--- change before his turn, that is, when it is the turn of
--- eloise. This is done by setting vartochange-a to either 1 or
--- 2. Then Abelard can set ap1 (next(ap1)) to either true or false,
--- when vartochange = 1, it is his turn (turn = a), and Phi is not
--- true. Abelard can set ap2 (next(ap2)) to either true or false, when
--- vartochange = 2, it is his turn (turn = a), and Phi is not true.
VAR
vartochange-a : {1,2};
ap1 : boolean;
ap2 : boolean;
ASSIGN
init(vartochange-a) := {1,2};
init(ap1) := FALSE;
init(ap2) := FALSE;
next(vartochange-a) := (!Phi & turn = e) ? {1,2}: vartochange-a;
next(ap1) := (!Phi & turn = a & vartochange-a = 1) ? {TRUE, FALSE} : ap1;
next(ap2) := (!Phi & turn = a & vartochange-a = 2) ? {TRUE, FALSE} : ap2;
MODULE eloise(turn, Phi)
--- Eloise controls only one variable ep1. Its initial value is set to
--- false. Eloise can set the value of ep1 (next(ep1)) to either true
--- or false, whenever it is her turn (turn = e) and Phi is not
--- true. Since she controls only one variable, the control variable
--- vartochange-e is dummy, but is used for uniformity with the MODULE
--- abelard.
VAR
vartochange-e : {1};
ep1 : boolean;
ASSIGN
init(ep1) := FALSE;
next(ep1) := (!Phi & turn = e & vartochange-e = 1) ? {TRUE, FALSE} : ep1;
MODULE main
VAR
turn : {e,a};
nowin : boolean;
--- We consider here a Peek instance where Eloise controls ep1, and
--- Abelard controls ap1 and ap2. The valuation to start with is
--- empty: ep1, ap1, and ap2 are all set to false. In other words, elo
--- is an instance of the module eloise, and abe is an instance of the
--- module abelard; both defined in this file.
elo : eloise(turn, Phi);
abe : abelard(turn, Phi);
DEFINE
--- In the Peek instance we consider, Abelard plays first (Tau =
--- A). The objective formula Phi is ep1 & ap1.
Phi := (elo.ep1) & (abe.ap2);
Tau := a;
ASSIGN
init(turn) := Tau;
init(nowin) := TRUE;
next(turn) :=
case
(turn = e) : a;
(turn = a) : e;
esac;
next(nowin) := Phi ? FALSE : nowin;
CTLSPEC
--- This formula is an immediate translation of the DL-PA formula in
--- (Balbiani, Herzig, Troquard, 2013 LICS) into the language of CTL.
AG (nowin -> (
!Phi &
((turn = e) -> AX nowin) &
((turn = a) -> EX nowin)
)
)