1/*
    2Model checker for fuzzy formulas in generalized probabilistic logic (GPL).
    3GPL is an expressive logic based on the modal mu-calculus for probabilistic 
    4systems.
    5GPL is designed for model checking reactive probabilistic transition systems 
    6(RPLTS).
    7From
    8Gorlin, Andrey, C. R. Ramakrishnan, and Scott A. Smolka. "Model checking with probabilistic tabled logic programming." Theory and Practice of Logic Programming 12.4-5 (2012): 681-700.
    9This program was kindly provided by Andrey Gorlin and adapted to MCINTYRE 
   10by Fabrizio Riguzzi.
   11*/

   18:- use_module(library(mcintyre)).   19
   20:- if(current_predicate(use_rendering/1)).   21:- use_rendering(c3).   22:- endif.   23:- dynamic kr/1,num/1.   24:- mc.   25
   26:- begin_lpad.   27
   28% models(S,F,H,W)
   29%   S: is a state of an RPLTS
   30%   F: is a GPL formula
   31%   H: is the history of actions (list)
   32models(_S, tt, _).
   33models(S, form(X), H) :-
   34	fdef(X, F),
   35	models(S, F, H).
   36models(S, and(F1,F2), H) :-
   37	models(S, F1, H),
   38	models(S, F2, H).
   39models(S, or(F1,F2), H) :-
   40	models(S, F1, H);
   41	models(S, F2, H).
   42models(S, diam(A, F), H) :-
   43	trans(S, A, SW),
   44	msw(SW, H, T),
   45	models(T, F, [T,SW|H]).
   46models(S, box(A, F), H) :-
   47	findall(SW, trans(S,A,SW), L),
   48	all_models(L, S, F, H).
   49
   50all_models([], _, _, _H).
   51all_models([SW|Rest], S, F, H) :-
   52	msw(SW, H, T),
   53	models(T,F,[T,SW|H]),
   54	all_models(Rest, S, F, H).
   55
   56% Prob. formulas of GPL are omitted
   57% Negated formulas are omitted
   58
   59
   60temporal(tabled_models(_,_,_)).
   61
   62% This is a simple example with entanglement that can scale the
   63% formula and the model.  Here, t is essentially a step down.
   64%
   65% The formula x can take values from 2 to 7.  When it's at 2:
   66%
   67% x = (<b>x /\ <c>t) \/ (<b>t /\ <c>x) \/ (<b>t /\ <c>t),
   68%
   69% t = [a]x \/ <b>[a]x
   70
   71% trans(s1(N), a, s1(N, a)).
   72% trans(s1(N), b, s1(N, b)).
   73% trans(s1(N), c, s1(N, c)).
   74% trans(s1(N), d, s1(N, d)).
   75trans(s1(N), A, s1(N, A)).
   76trans(s2(N), a, s2(N, a)) :- N>0.
   77
   78% values(s1(_N, a), [s3]).
   79% values(s1(N, b), [s1(N), s2(N)]).
   80% values(s1(N, c), [s1(N), s2(N)]).
   81values(s1(_N, a), [s3]) :- !.
   82values(s1(N, _A), [s1(N), s2(N)]).
   83values(s2(N, a), [s1(M)]) :- M is N-1.
   84
   85% set_sw(s1(_N, a), [1]).
   86% set_sw(s1(_N, b), [0.3, 0.7]).
   87% set_sw(s1(_N, c), [0.5, 0.5]).
   88set_sw(s1(_N, a), [1]) :- !.
   89set_sw(s1(_N, b), [0.2, 0.8]) :- !.
   90set_sw(s1(_N, _A), [0.1, 0.9]).
   91set_sw(s2(_N, a), [1]).
   92
   93msw(SW,H,V):-
   94  values(SW,L),
   95  append(L0,[LastV],L),
   96  set_sw(SW,PH),
   97  append(PH0,[_LastP],PH),
   98  foldl(pick_value(SW,H),PH0,L0,(1,_),(_,V)),
   99  (var(V)->  
  100    V=LastV
  101  ;
  102    true
  103  ).
  104
  105pick_value(_SW,_H,_PH,_I,(P0,V0),(P0,V0)):-
  106  nonvar(V0).
  107
  108pick_value(SW,H,PH,I,(P0,V0),(P1,V1)):-
  109  var(V0),
  110  PF is PH/P0,
  111  (prob_fact(SW,H,I,PF)->
  112    P1=PF,
  113    V1=I
  114  ;
  115    P1 is P0*(1-PF),
  116    V1=V0
  117  ).
  118
  119prob_fact(_,_,_,P):P.
  120
  121% Formulae:
  122letter(1, b).
  123letter(2, c).
  124letter(3, d).
  125letter(4, e).
  126letter(5, f).
  127letter(6, g).
  128letter(7, h).
  129
  130ex_conj(1, N, F, diam(b, form(G))) :- !,
  131        (N==1
  132        -> G=F
  133        ;  G=t(F)
  134        ).
  135ex_conj(N, C, F, and(diam(L, form(G)), Fs)) :-
  136        M is N-1,
  137        letter(N, L),
  138        ex_conj(M, C, F, Fs),
  139        (N==C
  140        -> G=F
  141        ;  G=t(F)
  142        ).
  143
  144ex_disj(N, 0, F, Fs) :- !,
  145        ex_conj(N, 0, F, Fs).
  146ex_disj(N, C, F, or(G, Fs)) :-
  147        M is C-1,
  148        ex_conj(N, C, F, G),
  149        ex_disj(N, M, F, Fs).
  150
  151fdef(x(N), F) :-
  152        ex_disj(N, N, x(N), F).
  153
  154fdef(t(F), or(box(a, form(F)), diam(b, form(n(F))))).
  155
  156fdef(n(F), box(a, form(F))).
  157
  158:-end_lpad.