```    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*/
```

?- `mc_sample(models(en(0), form(x), []),20,P)`. % expected result 1 % The values for en can be 0+. ?- `mc_sample(models(en(1), form(x), []),1, P)`. % expected result 1 */

```   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
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