/////////////////////////////////////////////////////////////////////////////////////////
// Example of logic programming Petri net (LPPN)
/////////////////////////////////////////////////////////////////////////////////////////
//
//   e2        c1(A)      e1(A)     c2(A)                  c5(A)
// [ t2 ]<----( p1 )---->[ t1 ]---->( p2 )---->[*dt1*]---->( p5 )
//                         |
//                         v
//                       (*dp1*)
//                         |
//                         v
//            ( p4 )---->[ t3 ]---->( p3 )
//            c4(B)       e3(A)    c3(A, B)
//
//
// with only c1(a) in p1
// expected execution paths:
// c1(a) --e2--> not c1(a)
// c1(a) --e1(a)--> not c1(a), c2(a), c5(a)
//
// with also c4(b) in p4
// c1(a) --e2--> not c1(a)
// c1(a) --e1(a), e3(a)--> not c1(a), c2(a), c5(a), not c4(b), c3(a, b)
//
/////////////////////////////////////////////////////////////////////////////////////////

// define a temporal range for the execution
time(0..1).

#domain fluent(F), event(E), time(N), time(N1), time(N2), time(N3).
#domain place(P), trans(T), trans(T1), trans(T2).

holdsAt(F, P, N) :-
  initially(F, P),
  not clipped(0, F, P, N).
holdsAt(F, P, N2) :- firesAt(E, T, N1), N1 < N2,
  initiates(T, F, P, N1),
  not clipped(N1, F, P, N2).
clipped(N1, F, P, N2) :- firesAt(E, T, N), N1 <= N, N < N2,
  terminates(T, F, P, N).

// execution semantics
{prefiresAt(T, N)} :- enabled(T, N), safe(T).
someTransitionPrefiresAt(N) :- prefiresAt(T, N).
:- N > 0, not someTransitionPrefiresAt(N-1).
:- prefiresAt(T1, N), prefiresAt(T2, N), T1 != T2.

#domain a(A), b(B).

// for each positive literal for place labels, type it as fluent (condition)
fluent(c1(A)).
fluent(c2(A)).
fluent(c3(A, B)).
fluent(c4(B)).
fluent(c5(A)).

// for each positive literal for event labels, type it as event
event(e1(A)).
event(e2).
event(e3(A)).

// for each place, type it and say how it is initially filled, type the identifiers
place(p1). initially(c1(a), p1). a(a).
place(p2).
place(p3).
place(p4). initially(c4(b), p4). b(b).

// for each place, type it and say if it is safe or not
trans(t1). safe(t1).
trans(t2). safe(t2).
trans(t3).

// for each place with more than one input,
// you cannot consume more than the only available token
:- 2{terminates(t1, c1(A), p1, N), terminates(t2, c1(A), p1, N)}.

// for each transition,
// define the conditions for being enabled
enabled(t1, N) :- holdsAt(c1(A), p1, N).
enabled(t2, N) :- holdsAt(c1(A), p1, N).
enabled(t3, N) :- holdsAt(c4(B), p4, N).

// for each transition,
// define how the substitution is decided
appliesAt(t1, subs(A), N) :- holdsAt(c1(A), p1, N), firesAt(e1(A), t1, N).
appliesAt(t2, subs(A), N) :- holdsAt(c1(A), p1, N), firesAt(e2, t2, N).
appliesAt(t3, subs(A, B), N) :- holdsAt(c4(B), p4, N), firesAt(e3(A), t3, N).

// for each safe transition,
// define the conditions for transforming the prefiring in firing
firesAt(e1(A), t1, N) :- holdsAt(c1(A), p1, N), prefiresAt(t1, N).
firesAt(e2, t2, N) :- holdsAt(c1(A), p1, N), prefiresAt(t2, N).

// for each transition,
// define how to create tokens in the output places
initiates(t1, c2(A), p2, N) :- appliesAt(t1, subs(A), N).
initiates(t3, c3(A, B), p3, N) :- appliesAt(t3, subs(A, B), N).

// for each transition, define how to consume tokens in the output places
terminates(t1, c1(A), p1, N) :- appliesAt(t1, subs(A), N).
terminates(t2, c1(A), p1, N) :- appliesAt(t2, subs(A), N).
terminates(t3, c4(B), p4, N) :- appliesAt(t3, subs(A, B), N).

// for each logic operator on places, specify the constraint
holdsAt(c5(A), p5, N) :- holdsAt(c2(A), p2, N).

// for each logic operator on transitions, specify the constraint
firesAt(e3(A), t3, N) :- holdsAt(c4(B), p4, N), firesAt(e1(A), t1, N).