Dynamic Predicates: table_prob0/2 table_prob1/2

227 Lines

17 Predicates

7 Exports

4 Imports

Imports	Exports
Name: {}/1 Module: clpr Name: xtl_transition/4 Module: xtl_interface Name: visited_expression/2 Module: state_space Name: visited_expression_id/1 Module: state_space	Name: sat/1 Name: sat/2 Name: search_prob0/3 Name: prob0/3 Name: prob1/3 Name: table_prob0/2 Name: state/1

Imports

Exports

Name: {}/1

Module: clpr

Name: xtl_transition/4

Module: xtl_interface

Name: visited_expression/2

Module: state_space

Name: visited_expression_id/1

Module: state_space

Name: sat/1

Name: sat/2

Name: search_prob0/3

Name: prob0/3

Name: prob1/3

Name: table_prob0/2

Name: state/1

Predicates

Predicates:

transition_probability/3

add_prob/3

add_prob([],_,0.0).

add_prob([State|List_States],E,P_phi_new) :-
    (transition_probability(E,State,P) -> P_trans = P
    ; P_trans=0.0
    ),
    add_prob(List_States,E,P_phi),
    P_phi_new is P_phi + P_trans.

Calls:

Name: is/2
Name: RECURSIVE_CALL/3	Module: dtmc_model_checking
Name: =/2
Name: transition_probability/3	Module: dtmc_model_checking
Name: ->/3

Called:

Name: prob_calc/3

Module: dtmc_model_checking

add_prob_prime/6

add_prob_prime(0.0,[],_,_,_,_).

add_prob_prime(P_phi_new,[S|List_S],E,F,G,K) :-
    transition_probability(E,S,P_trans),
    prob_calc(u(F,K,G),S,P_mat),
    add_prob_prime(P_phi,List_S,E,F,G,K),
    P_phi_new is P_trans*P_mat + P_phi.

Calls:

Name: is/2
Name: RECURSIVE_CALL/6	Module: dtmc_model_checking
Name: prob_calc/3	Module: dtmc_model_checking
Name: transition_probability/3	Module: dtmc_model_checking

Called:

Name: prob_calc/3

Module: dtmc_model_checking

against/3

against(P_phi,P,eq) :- P_phi = P.

against(P_phi,P,inf) :- P_phi =< P.

against(P_phi,P,sup) :- P_phi >= P.

against(P_phi,P,sinf) :- P_phi < P.

against(P_phi,P,ssup) :- P_phi > P.

against(P_phi,P,not(inf)) :- against(P_phi,P,ssup).

against(P_phi,P,not(sup)) :- against(P_phi,P,sinf).

against(P_phi,P,not(sinf)) :- against(P_phi,P,sup).

against(P_phi,P,not(ssup)) :- against(P_phi,P,inf).

Calls:

Name: RECURSIVE_CALL/3	Module: dtmc_model_checking
Name: >/2
Name: </2
Name: >=/2
Name: =</2
Name: =/2

Called:

Name: sat/2

Module: dtmc_model_checking

find_prob_u/4

find_prob_u([E],[P],E,P).

find_prob_u([S1,S2|List_S],[Prob1,Prob2|P_vect],E,P) :-
(E=S1,P=Prob1)
; find_prob_u([S2|List_S],[Prob2|P_vect],E,P).

Calls:

Name: RECURSIVE_CALL/4	Module: dtmc_model_checking
Name: =/2

Called:

Name: prob_calc/3

Module: dtmc_model_checking

prob0/3

prob0(_F,_G,E) :-
    table_prob0(E,true),!.

prob0(_F,G,E) :-
    sat(G,E),
    !,
    asserta(table_prob0(E,true)).

prob0(F,G,E1) :-
    sat(F,E1),
    assertz(table_prob0(E1,computing)),
    trans(E1,E2,_P),
    \+ table_prob0(E2,computing),
    (prob0(F,G,E2) ->
    asserta(table_prob0(E1,true)),
    retract(table_prob0(E1,computing))
    ),!.

Calls:

Name: !
Name: table_prob0/2	dynamic predicate
Name: retract/1
Name: asserta/1
Name: RECURSIVE_CALL/3	Module: dtmc_model_checking
Name: ->/2
Name: not/1
Name: trans/3	Module: foo_error
Name: assertz/1
Name: sat/2	Module: dtmc_model_checking

Called:

Name: search_prob0/3

Module: dtmc_model_checking

prob1/3

prob1(_F,_G,E) :-
    table_prob1(E,true),!.

prob1(_F,_G,E) :-
    \+(table_prob0(E,true)),
    !,
    asserta(table_prob1(E,true)).

prob1(F,G,E1) :-
    sat(F,E1),
    assert(table_prob1(E1,computing)),
    trans(E1,E2,_P),
    \+ table_prob1(E2,computing),
    (prob1(F,G,E2) ->
    asserta(table_prob1(E1,true)),
    retract(table_prob1(E1,computing))),!.

Calls:

Name: !
Name: table_prob1/2	dynamic predicate
Name: retract/1
Name: asserta/1
Name: RECURSIVE_CALL/3	Module: dtmc_model_checking
Name: ->/2
Name: not/1
Name: trans/3	Module: foo_error
Name: assert/1
Name: sat/2	Module: dtmc_model_checking
Name: table_prob0/2	dynamic predicate

prob_calc/3

prob_calc(x(F),E,P_phi) :-
    findall(S,(state(S),sat(F,S)),List_S),
    add_prob(List_S,E,P_phi).

prob_calc(u(_F,0,G),E,P_phi) :-
    (sat(G,E) -> P_phi=1.0
    ; P_phi=0.0
).

prob_calc(u(F,K_new,G),E,P_phi) :-
    K_new > 0,
    state(E),
    (sat(G,E) -> P_phi=1.0
    ; (sat(not(F),E) -> P_phi=0.0
    ; K is K_new -1 ,
    findall(S,trans(E,S,_),List_S),
    add_prob_prime(P_phi,List_S,E,F,G,K)
)
).

prob_calc(u(F,G),E,P_phi) :-
    retractall(table_prob0(_,_)),
    retractall(table_prob1(_,_)),
    % retractall(good_search(_C)),
    prob_calc_u1(F,G,List_S,P_vect),
    state(E),
    (find_prob_u(List_S,P_vect,E,P) -> P_phi=P
    ; P_phi=0.0
).

prob_calc(f(K,F),E,P_phi) :-
    prob_calc(u(true,K,F),E,P_phi).

prob_calc(f(F),E,P_phi) :-
    prob_calc(u(true,F),E,P_phi).

Calls:

Name: RECURSIVE_CALL/3	Module: dtmc_model_checking
Name: =/2
Name: find_prob_u/4	Module: dtmc_model_checking
Name: ->/3
Name: state/1	Module: dtmc_model_checking
Name: prob_calc_u1/4	Module: dtmc_model_checking
Name: retractall/1
Name: add_prob_prime/6	Module: dtmc_model_checking
Name: findall/3
Name: is/2
Name: sat/2	Module: dtmc_model_checking
Name: >/2
Name: add_prob/3	Module: dtmc_model_checking

Called:

Name: add_prob_prime/6	Module: dtmc_model_checking
Name: sat/2	Module: dtmc_model_checking

prob_calc_u1/4

prob_calc_u1(F,G,List_S,P_vect) :-
    findall(S,(state(S),search_prob0(F,G,S)),List_S),
    findall(E,(state(E),prob1(F,G,E)),_List),
    prob_calc_u2(F,G,List_S,List_S,P_vect,P_vect).

Calls:

Name: prob_calc_u2/6	Module: dtmc_model_checking
Name: findall/3

Called:

Name: prob_calc/3

Module: dtmc_model_checking

prob_calc_u2/6

prob_calc_u2(_F,_G,[],_List_S,[],_P_vect).

prob_calc_u2(F,G,[S|List_S_explored],List_S,[P_phi|P_vect_explored],P_vect) :-
    (table_prob1(S,true) -> prob_calc_u3(S,List_S,P_phi,P_vect)
    ; P_phi=1.0
    ),
    prob_calc_u2(F,G,List_S_explored,List_S,P_vect_explored,P_vect).

Calls:

Name: RECURSIVE_CALL/6	Module: dtmc_model_checking
Name: =/2
Name: prob_calc_u3/4	Module: dtmc_model_checking
Name: table_prob1/2	dynamic predicate
Name: ->/3

Called:

Name: prob_calc_u1/4

Module: dtmc_model_checking

prob_calc_u3/4

prob_calc_u3(_S,[],0.0,[]).

prob_calc_u3(S,[E|List_S],P_phi_new,[P|P_vect]) :-
    prob_calc_u3(S,List_S,P_phi,P_vect),
    (transition_probability(S,E,P_trans) -> {P_phi_new = P*P_trans + P_phi}
    ; P_phi_new=P_phi
).

Calls:

Name: =/2
Name: {}/1	Module: clpr
Name: transition_probability/3	Module: dtmc_model_checking
Name: ->/3
Name: RECURSIVE_CALL/4	Module: dtmc_model_checking

Called:

Name: prob_calc_u2/6

Module: dtmc_model_checking

sat/1

sat(Formula) :- start(E), sat(Formula,E).

Calls:

Name: sat/2	Module: dtmc_model_checking
Name: start/1	Module: dtmc_model_checking

Called:

Name: prob0/3	Module: dtmc_model_checking
Name: prob_calc/3	Module: dtmc_model_checking
Name: prob1/3	Module: dtmc_model_checking
Name: sat/1	Module: dtmc_model_checking
Name: sat_not/2	Module: dtmc_model_checking

sat/2

sat(true,_E).

sat(false,_E):-fail.

sat(p(Property),E) :- check_ap(Property,E).

sat(and(F,G),E) :- sat(F,E), sat(G,E).

sat(or(F,_G),E) :- sat(F,E).

sat(or(_F,G),E) :- sat(G,E).

sat(imp(F,G),E) :- sat(or(not(F),G),E).

sat(not(F),E) :- prob_formula(_,_,_)\=F,sat_not(F,E).

sat(prob_formula(Operator,P,Ctl_formula),E) :-
    prob_calc(Ctl_formula,E,P_phi),
    against(P_phi,P,Operator).

sat(not(prob_formula(Operator,P,Ctl_formula)),E) :-
    sat(prob_formula(not(Operator),P,Ctl_formula),E).

sat(prob_formula(Operator,P,g(K,F)),E) :-
    Q is 1-P,
    sat(not(prob_formula(Operator,Q,f(K,not(F)))),E).

sat(prob_formula(Operator,P,g(F)),E) :-
    Q is 1-P,
    sat(not(prob_formula(Operator,Q,f(not(F)))),E).

Calls:

Name: RECURSIVE_CALL/2	Module: dtmc_model_checking
Name: is/2
Name: against/3	Module: dtmc_model_checking
Name: prob_calc/3	Module: dtmc_model_checking
Name: sat_not/2	Module: dtmc_model_checking
Name: \=/2
Name: check_ap/2	Module: foo_error
Name: fail

Called:

Name: prob0/3	Module: dtmc_model_checking
Name: prob_calc/3	Module: dtmc_model_checking
Name: prob1/3	Module: dtmc_model_checking
Name: sat/1	Module: dtmc_model_checking
Name: sat_not/2	Module: dtmc_model_checking

sat_not/2

sat_not(false,_E).

sat_not(true,_E) :- fail.

sat_not(p(Property),E) :- \+(check_ap(Property,E)).

sat_not(and(F,_G),E) :- sat_not(F,E).

sat_not(and(_F,G),E) :- sat_not(G,E).

sat_not(or(F,G),E) :- sat_not(F,E),sat_not(G,E).

sat_not(imp(F,G),E) :- sat(not(or(not(F),G)),E).

sat_not(not(F),E) :- sat(F,E).

Calls:

Name: sat/2	Module: dtmc_model_checking
Name: RECURSIVE_CALL/2	Module: dtmc_model_checking
Name: check_ap/2	Module: foo_error
Name: not/1
Name: fail

Called:

Name: sat/2

Module: dtmc_model_checking

search_prob0/3

search_prob0(F,G,E):-
retractall(table_prob0(_,computing)),
prob0(F,G,E).

Calls:

Name: prob0/3	Module: dtmc_model_checking
Name: retractall/1

start/1

start(root).

Called:

Name: sat/1

Module: dtmc_model_checking

state/1

state(X) :- visited_expression_id(X).

Calls:

Name: visited_expression_id/1

Module: state_space

Called:

Name: prob_calc/3

Module: dtmc_model_checking

transition_probability/3

transition_probability(From,To,Prob) :- trans(From,To,_),
    visited_expression(From,FS),
    visited_expression(To,TS),
    xtl_transition(FS,_,TS,Infos),
    (member(probability/X,Infos) -> Prob=X ; write(no_probability(Infos)),nl,fail).

Calls:

Name: fail
Name: nl
Name: write/1
Name: =/2
Name: member/2
Name: ->/3
Name: xtl_transition/4	Module: xtl_interface
Name: visited_expression/2	Module: state_space
Name: trans/3	Module: foo_error

Called:

Name: add_prob_prime/6	Module: dtmc_model_checking
Name: add_prob/3	Module: dtmc_model_checking
Name: prob_calc_u3/4	Module: dtmc_model_checking

Determinacy Checker

Determinacy Checker:

! Existence error in argument 1 of absolute_file_name/3
! file probsrc(xtl_interface) does not exist
! goal: absolute_file_name(probsrc(xtl_interface),_261,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/extensions/markov/dtmc_model_checking.pl')])

dtmc_model_checking

prob_prolog/extensions/markov/dtmc_model_checking.pl

Modules

Predicates of dtmc_model_checking

Module Information

Dynamic Predicates: table_prob0/2 table_prob1/2

227 Lines

17 Predicates

7 Exports

4 Imports

Predicates:

add_prob/3

add_prob_prime/6

against/3

find_prob_u/4

prob0/3

prob1/3

prob_calc/3

prob_calc_u1/4

prob_calc_u2/6

prob_calc_u3/4

sat/1

sat/2

sat_not/2

search_prob0/3

start/1

state/1

transition_probability/3

Determinacy Checker: