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

?- `mc_sample(models(s1(3), form(x(2)), []),10,P)`. % expected result 1 % The values for s1 can be 0+, and for x from 2 to 7. */

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