cplint on
SWI
SH
is a web application for probabilistic logic programming
About
Help
LIFTCOVER-Help
PHIL-Help
PASCAL-Help
Credits
Dismiss
Latest:
Threads and Python in LIFTCOVER
,
course
,
PHIL examples
,
book
Toggle navigation
?
users online
Logout
Open hangout
Open chat for current file
/* Model checker for fuzzy formulas in generalized probabilistic logic (GPL). GPL is an expressive logic based on the modal mu-calculus for probabilistic systems. GPL is designed for model checking reactive probabilistic transition systems (RPLTS). From Gorlin, 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. This program was kindly provided by Andrey Gorlin and adapted to MCINTYRE by Fabrizio Riguzzi. */ /** <examples> ?- 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. */ :- use_module(library(mcintyre)). :- if(current_predicate(use_rendering/1)). :- use_rendering(c3). :- endif. :- dynamic kr/1,num/1. :- mc. :- begin_lpad. % models(S,F,H,W) % S: is a state of an RPLTS % F: is a GPL formula % H: is the history of actions (list) models(_S, tt, _). models(S, form(X), H) :- fdef(X, F), models(S, F, H). models(S, and(F1,F2), H) :- models(S, F1, H), models(S, F2, H). models(S, or(F1,F2), H) :- models(S, F1, H); models(S, F2, H). models(S, diam(A, F), H) :- trans(S, A, SW), msw(SW, H, T), models(T, F, [T,SW|H]). models(S, box(A, F), H) :- findall(SW, trans(S,A,SW), L), all_models(L, S, F, H). all_models([], _, _, _H). all_models([SW|Rest], S, F, H) :- msw(SW, H, T), models(T,F,[T,SW|H]), all_models(Rest, S, F, H). % Prob. formulas of GPL are omitted % Negated formulas are omitted temporal(tabled_models(_,_,_)). % This is a simple example with entanglement that can scale the % formula and the model. Here, t is essentially a step down. % % The formula x can take values from 2 to 7. When it's at 2: % % x = (<b>x /\ <c>t) \/ (<b>t /\ <c>x) \/ (<b>t /\ <c>t), % % t = [a]x \/ <b>[a]x % trans(s1(N), a, s1(N, a)). % trans(s1(N), b, s1(N, b)). % trans(s1(N), c, s1(N, c)). % trans(s1(N), d, s1(N, d)). trans(s1(N), A, s1(N, A)). trans(s2(N), a, s2(N, a)) :- N>0. % values(s1(_N, a), [s3]). % values(s1(N, b), [s1(N), s2(N)]). % values(s1(N, c), [s1(N), s2(N)]). values(s1(_N, a), [s3]) :- !. values(s1(N, _A), [s1(N), s2(N)]). values(s2(N, a), [s1(M)]) :- M is N-1. % set_sw(s1(_N, a), [1]). % set_sw(s1(_N, b), [0.3, 0.7]). % set_sw(s1(_N, c), [0.5, 0.5]). set_sw(s1(_N, a), [1]) :- !. set_sw(s1(_N, b), [0.2, 0.8]) :- !. set_sw(s1(_N, _A), [0.1, 0.9]). set_sw(s2(_N, a), [1]). msw(SW,H,V):- values(SW,L), append(L0,[LastV],L), set_sw(SW,PH), append(PH0,[_LastP],PH), foldl(pick_value(SW,H),PH0,L0,(1,_),(_,V)), (var(V)-> V=LastV ; true ). pick_value(_SW,_H,_PH,_I,(P0,V0),(P0,V0)):- nonvar(V0). pick_value(SW,H,PH,I,(P0,V0),(P1,V1)):- var(V0), PF is PH/P0, (prob_fact(SW,H,I,PF)-> P1=PF, V1=I ; P1 is P0*(1-PF), V1=V0 ). prob_fact(_,_,_,P):P. % Formulae: letter(1, b). letter(2, c). letter(3, d). letter(4, e). letter(5, f). letter(6, g). letter(7, h). ex_conj(1, N, F, diam(b, form(G))) :- !, (N==1 -> G=F ; G=t(F) ). ex_conj(N, C, F, and(diam(L, form(G)), Fs)) :- M is N-1, letter(N, L), ex_conj(M, C, F, Fs), (N==C -> G=F ; G=t(F) ). ex_disj(N, 0, F, Fs) :- !, ex_conj(N, 0, F, Fs). ex_disj(N, C, F, or(G, Fs)) :- M is C-1, ex_conj(N, C, F, G), ex_disj(N, M, F, Fs). fdef(x(N), F) :- ex_disj(N, N, x(N), F). fdef(t(F), or(box(a, form(F)), diam(b, form(n(F))))). fdef(n(F), box(a, form(F))). :-end_lpad.