```    1/*
2Model checking of a Markov chain: we want to know what is the likelihood
3that on an execution of the chain from a start state s, a final state t
4will be reached?
5From
6Gorlin, 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.
7*/
8
9:- use_module(library(pita)).   10
11:- if(current_predicate(use_rendering/1)).   12:- use_rendering(c3).   13:- use_rendering(graphviz).   14:- endif.   15
16:- pita.   17
18:- set_pita(depth_bound,true).   19:- set_pita(depth,5).   20
21
24% reach(S, I, T) starting at state S at instance I,
25%   state T is reachable.
26reach(S, I, T) :-
27  trans(S, I, U),
28  reach(U, next(I), T).
29
30reach(S, _, S).
31
32% trans(S,I,T) transition from S at instance I goes to T
33
34trans(s0,S,s0):0.5; trans(s0,S,s1):0.3; trans(s0,S,s2):0.2.
35
36trans(s1,S,s1):0.4; trans(s1,S,s3):0.1; trans(s1,S,s4):0.5.
37
38trans(s4,_,s3).
41markov_chain(digraph(G)):-
42    findall(edge(A -> B,[label=P]),
43      (clause(trans(A,_,B,_,_,_),
44        (get_var_n(_,_,_,_,Probs,_),equalityc(_,_,N,_))),
45        nth0(N,Probs,P)),
46      G0),
47    findall(edge(A -> B,[label=1.0]),
48      clause(trans(A,_,B,_,_,_),onec(_,_)),
49      G1),
50    append(G0,G1,G).```

?- `prob(reach(s0,0,s0),P)`. % expecte result ~ 1.

?- `prob(reach(s0,0,s1),P)`. % expecte result ~ 0.5984054054054054.

?- `prob(reach(s0,0,s2),P)`. % expecte result ~ 0.4025135135135135.

?- `prob(reach(s0,0,s3),P)`. % expecte result ~ 0.5998378378378378.

?- `prob(reach(s0,0,s4),P)`. % expecte result ~ 0.49948717948717947.

?- `prob(reach(s1,0,s0),P)`. % expecte result ~ 0.

?- `markov_chain(G)`. % draw the Markov chain */