% A specification of Modal Logic for pi-calculus.
% Based on the paper "Modal logics for mobile processes", Milner et.al. 
% TCS 114 (1993).

% This definition file implements the specification of modal logics
% described in the paper:
%  Alwen Tiu. Model checking for pi-calculus using proof search.
%  Available online from http://www.loria.fr/~tiu 
%
% Dependency: this file needs the pi.def (definition of late transition
% system for pi-calculus)

% Assume the formulas in the modal logic are in negation normal form.
% 

include "pi.def".


% A "lazy" but incomplete encoding.

sat P top.
sat P (and A B) := sat P A, sat P B.
sat P (or A B) := sat P A ; sat P B.
sat P (boxMatch X Y A) := (X = Y) => sat P A.
sat P (diaMatch X Y A) := (X = Y), sat P A.
sat P (boxAct X A) := pi P1\ one P X P1 => sat P1 A.
sat P (diaAct X A) := sigma P1\ one P X P1, sat P1 A.
sat P (boxOut X A) := pi Q\ onep P (up X) Q => nabla y\ sat (Q y) (A y).
sat P (diaOut X A) := sigma Q\ onep P (up X) Q, nabla y\ sat (Q y) (A y).
sat P (boxIn X A) := pi Q\ onep P (dn X) Q => pi y\ sat (Q y) (A y).
sat P (diaIn X A) := sigma Q\ onep P (dn X) Q, sigma y\ sat (Q y) (A y).
sat P (boxInL X A) := pi Q\ onep P (dn X) Q => sigma y\ sat (Q y) (A y).
sat P (diaInL X A) := sigma Q\ onep P (dn X) Q, pi y\ sat (Q y) (A y).
sat P (boxInE X A) := sigma y\ pi Q\ onep P (dn X) Q => sat (Q y) (A y).
sat P (diaInE X A) := pi y\ sigma Q\ onep P (dn X) Q, sat (Q y) (A y).

% Counterexample to the completeness of the above encoding: 

assert 1 (diaIn x (u\ (boxMatch x u bot))).
proc 1 (in x (y\ z)).

% This will generate an exception
test1 := proc 1 P, assert 1 A, sat P A.

%
% A complete encoding: using explicit list of names.
 
member X (cons Y L) := (X = Y) ; member X L.

lsat L P top.
lsat L P (and A B) := lsat L P A, lsat L P B.
lsat L P (or A B) := lsat L P A ; lsat L P B.
lsat L P (boxMatch X Y A) := (X = Y) => lsat L P A.
lsat L P (diaMatch X Y A) := (X = Y), lsat L P A.
lsat L P (boxAct X A) := pi P1\ one P X P1 => lsat L P1 A.
lsat L P (diaAct X A) := sigma P1\ one P X P1, lsat L P1 A.
lsat L P (boxOut X A) := pi Q\ onep P (up X) Q => nabla y\ lsat (cons y L) (Q y) (A y).
lsat L P (diaOut X A) := sigma Q\ onep P (up X) Q, nabla y\ lsat (cons y L) (Q y) (A y).
lsat L P (boxIn X A) := pi Q\ onep P (dn X) Q => 
         nabla w\ pi y\ (member y (cons w L) => lsat (cons w L) (Q y) (A y)).
lsat L P (diaIn X A) := sigma Q\ onep P (dn X) Q, 
         nabla w\ sigma y\ (member y (cons w L), lsat (cons w L) (Q y) (A y)).
lsat L P (boxInL X A) := pi Q\ onep P (dn X) Q => 
         nabla w\ sigma y\ (member y (cons w L), lsat (cons w L) (Q y) (A y)).
lsat L P (diaInL X A) := sigma Q\ onep P (dn X) Q, 
         nabla w\ pi y\ (member y (cons w L) => lsat (cons w L) (Q y) (A y)).
lsat L P (boxInE X A) := nabla w\ sigma y\ 
         (member y (cons w L), 
          pi Q\ onep P (dn X) Q => lsat (cons w L) (Q y) (A y)).
lsat L P (diaInE X A) := nabla w\ pi y\ member y (cons w L) => 
          sigma Q\ onep P (dn X) Q, lsat (cons w L) (Q y) (A y).

% The example above should now be provable

test2 := proc 1 P, assert 1 A, lsat (cons x nil) P A.