reachability.lp

%% instance

place(1).
place(2).
place(3).
place(4).
transition(1).
transition(2).
t_pre(1,1).
t_post(1,2).
t_test(1,1).
t_pre(2,3).
t_post(2,4).
m0(1).
m0(3).

mZ(2).
mZ(4).

%% model

#domain time(T).
#domain transition(R).
#domain place(P).
#const t_max=10.
time(0..t_max).

token(P,0) :- m0(P).

{ taken(R,T) } :-
    token(Pi,T):t_pre(R,Pi),
    token(Pi,T):t_test(R,Pi). % context test


token(P,T+1) :- t_post(R,P), taken(R,T).

:- 2 { taken(Trans,T):t_pre(Trans,P) }.
% uncomment for interleaving:  :- 2 { taken(Trans,T):transition(Trans) }.
token(P,T+1) :-token(P,T), 0 { taken(Trans,T):t_pre(Trans,P) } 0.

:- token(P,t_max), not mZ(P).
:- not token(P,t_max), mZ(P).

#minimize { taken(R,T) }.



#hide.
#show taken/2.
#show token/2.

unfolding.lp

% Knowledge

p(1..2).
t(1).
t_pre(1,1;2).
m0(1;2).

#base.

% BEGIN OF MODELCHECKER

% Definition of causality relation: X is cause of Y if X produces a
% condition that is consumed by Y
cause(X,Y) :- e_pre(Y,Z), e_post(X,Z).

% Marks the execution (or non execution) of events
exe(e(X1,X2)) :- exe(e(Y1,Y2)) : cause(e(Y1,Y2),e(X1,X2)),
	not nexe(e(X1,X2)), not cutoff(e(X1,X2)), e(X1,X2).
nexe(e(X1,X2)) :- not exe(e(X1,X2)), not cutoff(e(X1,X2)), e(X1,X2).

% Old conflict resolutor.
%
% This rule doesn't work in the contextual case, since we have to take
% into account that conflict not only does arise when two events have
% a common condition in their preset, but also when the other cases
% described by the asymmetric conflict relation arise.
%
:- 2{exe(X) : e_pre(X, b(Y1,Y2))}, b(Y1,Y2).

% This rule creates the marking for the configuration: condition X is
% marked if its preset Y event has been marked as executed and none of
% the events in its postset have been marked.
mark(b(X1, X2)) :- exe(Y) : e_post(Y, b(X1,X2)), nexe(Y) : e_pre(Y, b(X1,X2)), b(X1,X2).

% REACHABILITY
%
% Is the problem of finding whether a marking m is reachable from the
% original marking. We do this by removing all the possible models
% where a place in X is not marked.
%
% This rule marks the places in the original c-net whose image is
% marked in the unfolding
%
reachable(Y) :- mark(b(X,Y)), s(Y).

% END OF MODELCHECKER

e(0,0).
b(0,X) :- m0(X).

#cumulative i.

#volatile i.

% Generating possible extensions

e(i,X) :- t(X), e(i-1,Y), t_post(Y,Z), t_pre(X,Z), reachable(U) : t_pre(X, U).
b(i,X) :- e(i,Y), t(Y), t_post(Y,X).
e_post(e(i,Y), b(i,X)) :- e(i,Y), t(Y), t_post(Y,X).

%#base.

% alessandro@BloodyMary:~$ iclingo unfolder.lp
% % warning: e_pre/2 is never defined
% % warning: cutoff/1 is never defined
% % warning: s/1 is never defined
% % warning: t_post/2 is never defined

% ERROR: unstratified predicate in:
% unfolder.lp:33:1: mark(b(X1,X2)):-exe(Y):e_post(Y,b(X1,X2)),nexe(Y):e_pre(Y,b(X1,X2)),b(X1,X2).
% 	unfolder.lp:59:1: e_post/2