1		start(unlocked).
2		trans(lock,unlocked,locked,[probability/0.5]).
3		trans(skip,unlocked,unlocked,[probability/0.5]).
4		trans(unlock,locked,unlocked,[probability/0.5]).
5		trans(deadlock,locked,finished,[probability/0.5]).
6		prop(X,X).
7
8		% :pctl P>{0.999} [F {finished}]
9		%| ?- use_module(extension('markov/dtmc_model_checking.pl')).
10		% yes
11		% | ?- sat(prob_formula(eq,P,f(p(xtl_predicate_check(finished))))).
12		% P = 1.0 ?
13		% yes
14
15		/*
16		>>> :pctl P={p} [F {finished}]
17		Parsing temporal formula, kind=pctl, lge=none, formula="P={p} [F {finished}]"
18		Checking PCTL formula from state 0 : P={p} [F {finished}]
19		AST: probformula(equal,_225537,f(ap(xtl_predicate_check(finished))))
20		Open Probability Variables: [p/_225537]
21		PCTL Formula TRUE: P={p} [F {finished}]
22		PCTL Solutions: [p/1.0]
23
24
25		>>> :pctl not(P={p} [F {finished}])
26		Parsing temporal formula, kind=pctl, lge=none, formula="not(P={p} [F {finished}])"
27		Checking PCTL formula from state 0 : not(P={p} [F {finished}])
28		AST: not(probformula(equal,_11035,f(ap(xtl_predicate_check(finished)))))
29		Open Probability Variables: [p/_11035]
30		PCTL Formula TRUE: not(P={p} [F {finished}])
31		PCTL Solutions: [p/(1.0-2.3E-16)]
32
33		>>> :pctl P={p} [F<=5 {finished}]
34		Parsing temporal formula, kind=pctl, lge=none, formula="P={p} [F<=5 {finished}]"
35		Checking PCTL formula from state 0 : P={p} [F<=5 {finished}]
36		AST: probformula(equal,_11265,fk(5,ap(xtl_predicate_check(finished))))
37		Open Probability Variables: [p/_11265]
38		PCTL Formula TRUE: P={p} [F<=5 {finished}]
39		PCTL Solutions: [p/0.59375]
40
41		>>> :pctl P={p} [F<=1 {finished}]
42		Parsing temporal formula, kind=pctl, lge=none, formula="P={p} [F<=1 {finished}]"
43		Checking PCTL formula from state 0 : P={p} [F<=1 {finished}]
44		AST: probformula(equal,_11719,fk(1,ap(xtl_predicate_check(finished))))
45		Open Probability Variables: [p/_11719]
46		PCTL Formula TRUE: P={p} [F<=1 {finished}]
47		PCTL Solutions: [p/0.0]
48
49		>>> :pctl P={p} [F<=2 {finished}]
50		Parsing temporal formula, kind=pctl, lge=none, formula="P={p} [F<=2 {finished}]"
51		Checking PCTL formula from state 0 : P={p} [F<=2 {finished}]
52		AST: probformula(equal,_12173,fk(2,ap(xtl_predicate_check(finished))))
53		Open Probability Variables: [p/_12173]
54		PCTL Formula TRUE: P={p} [F<=2 {finished}]
55		PCTL Solutions: [p/0.25]
56
57		probcli SimpleMarkov.P -mc 10000 -nodead -pctlformulat 'P={0.25} [F<=2 {finished}]'
58		*/