Skip to content

Instantly share code, notes, and snippets.

@hoheinzollern
Created December 5, 2011 16:14
Show Gist options
  • Save hoheinzollern/1434129 to your computer and use it in GitHub Desktop.
Save hoheinzollern/1434129 to your computer and use it in GitHub Desktop.
%% 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.
% 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment