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
   22:- begin_lpad.   23
   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).
   39:- end_lpad.   40
   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).