1/*
    2Model checker for Recursive Markov Chains expressed in 
    3generalized probabilistic logic (GPL).
    4GPL is an expressive logic based on the modal mu-calculus for probabilistic 
    5systems.
    6GPL is designed for model checking reactive probabilistic transition systems 
    7(RPLTS).
    8From
    9Gorlin, 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.
   10This program was kindly provided by Andrey Gorlin and adapted to MCINTYRE 
   11by Fabrizio Riguzzi.
   12*/

   21:- use_module(library(mcintyre)).   22
   23:- if(current_predicate(use_rendering/1)).   24:- use_rendering(c3).   25:- endif.   26:- dynamic kr/1,num/1.   27:- mc.   28
   29:- begin_lpad.   30
   31% models(S,F,H,W)
   32%   S: is a state of an RPLTS
   33%   F: is a GPL formula
   34%   H: is the history of actions (list)
   35models(_S, tt, _).
   36models(S, form(X), H) :-
   37	fdef(X, F),
   38	models(S, F, H).
   39models(S, and(F1,F2), H) :-
   40	models(S, F1, H),
   41	models(S, F2, H).
   42models(S, or(F1,F2), H) :-
   43	models(S, F1, H);
   44	models(S, F2, H).
   45models(S, diam(A, F), H) :-
   46	trans(S, A, SW),
   47	msw(SW, H, T),
   48	models(T, F, [T,SW|H]).
   49models(S, box(A, F), H) :-
   50	findall(SW, trans(S,A,SW), L),
   51	all_models(L, S, F, H).
   52
   53all_models([], _, _, _H).
   54all_models([SW|Rest], S, F, H) :-
   55	msw(SW, H, T),
   56	models(T,F,[T,SW|H]),
   57	all_models(Rest, S, F, H).
   58
   59% Prob. formulas of GPL are omitted
   60% Negated formulas are omitted
   61
   62
   63% 1-exit RMC example for the slow-converging x = 1/2 (1 + x^2)
   64% equation, scaled to repeat it multiple times.
   65
   66fdef(x, or(diam(e, tt),
   67           or(diam(p, form(x)),
   68              and(diam(c, form(x)), diam(r, form(x)))))).
   69
   70trans(en(N), p, en(N, p)).
   71trans(ex(N), e, ex(N, e)).
   72trans(l1x(N), p, l1x(N, p)).
   73trans(l1e(N), c, l1e(N, c)).
   74trans(l1e(N), r, l1e(N, r)).
   75trans(l2x(N), p, l2x(N, p)).
   76trans(l2e(N), c, l2e(N, c)).
   77trans(l2e(N), r, l2e(N, r)).
   78trans(l3x(N), p, l3x(N, p)).
   79trans(l3e(N), c, l3e(N, c)).
   80trans(l3e(N), r, l3e(N, r)).
   81
   82values(en(0, p), [l1e(0), ex(0)]).
   83values(en(N, p), [l1e(N), l3e(N)]) :- N>0.
   84
   85values(ex(N, e), [ex(N)]).
   86
   87values(l1x(N, p), [l2e(N)]).
   88values(l1e(N, c), [en(N)]).
   89values(l1e(N, r), [l1x(N)]).
   90
   91values(l2x(0, p), [ex(0)]).
   92values(l2x(N, p), [l3e(N)]) :- N>0.
   93
   94values(l2e(N, c), [en(N)]).
   95values(l2e(N, r), [l2x(N)]).
   96
   97values(l3x(N, p), [ex(N)]).
   98
   99values(l3e(N, c), [en(M)]) :-
  100        N>0,
  101        M is N-1.
  102
  103values(l3e(N, r), [l3x(N)]).
  104
  105set_sw(en(_N, p), [0.5, 0.5]).
  106set_sw(ex(_N, e), [1]).
  107set_sw(l1x(_N, p), [1]).
  108set_sw(l1e(_N, c), [1]).
  109set_sw(l1e(_N, r), [1]).
  110set_sw(l2x(_N, p), [1]).
  111set_sw(l2e(_N, c), [1]).
  112set_sw(l2e(_N, r), [1]).
  113set_sw(l3x(_N, p), [1]).
  114set_sw(l3e(_N, c), [1]).
  115set_sw(l3e(_N, r), [1]).
  116
  117
  118
  119msw(SW,H,V):-
  120  values(SW,L),
  121  append(L0,[LastV],L),
  122  set_sw(SW,PH),
  123  append(PH0,[_LastP],PH),
  124  foldl(pick_value(SW,H),PH0,L0,(1,_),(_,V)),
  125  (var(V)->  
  126    V=LastV
  127  ;
  128    true
  129  ).
  130
  131pick_value(_SW,_H,_PH,_I,(P0,V0),(P0,V0)):-
  132  nonvar(V0).
  133
  134pick_value(SW,H,PH,I,(P0,V0),(P1,V1)):-
  135  var(V0),
  136  PF is PH/P0,
  137  (prob_fact(SW,H,I,PF)->
  138    P1=PF,
  139    V1=I
  140  ;
  141    P1 is P0*(1-PF),
  142    V1=V0
  143  ).
  144
  145prob_fact(_,_,_,P):P.
  146
  147
  148:-end_lpad.