Dynamic Predicates: node/1 prob_current/2 table_prob0/3 table_prob1/3

451 Lines

28 Predicates

8 Exports

12 Imports

Imports	Exports
Name: {}/1 Module: clpr Name: add_error/3 Module: error_manager Name: add_internal_error/2 Module: error_manager Name: add_warning/3 Module: error_manager Name: find_initialised_states/1 Module: state_space Name: current_state_id/1 Module: state_space Name: start_ms_timer/1 Module: tools Name: stop_ms_timer_with_msg/2 Module: tools Name: xtl_transition/4 Module: xtl_interface Name: visited_expression/2 Module: state_space Name: visited_expression_id/1 Module: state_space Name: safe_number_codes/2 Module: tools	Name: pctl_model_check/4 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: add_error/3

Module: error_manager

Name: add_internal_error/2

Module: error_manager

Name: add_warning/3

Module: error_manager

Name: find_initialised_states/1

Module: state_space

Name: current_state_id/1

Module: state_space

Name: start_ms_timer/1

Module: tools

Name: stop_ms_timer_with_msg/2

Module: tools

Name: xtl_transition/4

Module: xtl_interface

Name: visited_expression/2

Module: state_space

Name: visited_expression_id/1

Module: state_space

Name: safe_number_codes/2

Module: tools

Name: pctl_model_check/4

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:

pre_process_formula/4

transition_probability/3

against/3

against(P_phi,ReferenceP,equal) :- !,
    (ground_number(ReferenceP,P) ->
    P_phi =< P + 0.00000000000000023,
    P =< P_phi + 0.00000000000000023
    ; ReferenceP = P_phi % ReferenceP is an open variable
).

against(P_phi,ReferenceP,less) :-
    ground_number(ReferenceP,P), !,
    P_phi =< P + 0.00000000000000023. % less

against(P_phi,ReferenceP,greater) :-
    ground_number(ReferenceP,P), !,
    P_phi >= P - 0.00000000000000023. % greater

against(P_phi,ReferenceP,strictlyless) :-
    ground_number(ReferenceP,P), !,
    P_phi + 0.00000000000000023 < P . % strictly less

against(P_phi,ReferenceP,strictlygreater) :-
    ground_number(ReferenceP,P), !,
    P_phi - 0.00000000000000023 > P . % strictlygreater

against(P_phi,ReferenceP,not(equal)) :- !,
    (ground_number(ReferenceP,P) ->
    (P_phi > P + 0.00000000000000023 ;
    P =< P_phi + 0.00000000000000023
    )
    ; % ReferenceP is an open variable
    add_warning(dtmc_model_checking,'Using symbolic variable for inequality: ',P_phi),
    (P_phi < 1-0.00000000000000023
    -> ReferenceP = P_phi + 0.00000000000000023
    ; ReferenceP = P_phi - 0.00000000000000023
)
).

against(P_phi,P,not(less)) :- !, against(P_phi,P,strictlygreater).

against(P_phi,P,not(greater)) :- !, against(P_phi,P,strictlyless).

against(P_phi,P,not(strictlyless)) :- !, against(P_phi,P,greater).

against(P_phi,P,not(strictlygreater)) :- !, against(P_phi,P,less).

against(P1,P2,Op) :- add_internal_error('Illegal comparison operator: ',against(P1,P2,Op)),fail.

Calls:

Name: fail
Name: add_internal_error/2	Module: error_manager
Name: RECURSIVE_CALL/3	Module: dtmc_model_checking
Name: !
Name: =/2
Name: </2
Name: ->/3
Name: add_warning/3	Module: error_manager
Name: =</2
Name: >/2
Name: ground_number/2	Module: dtmc_model_checking
Name: >=/2

Called:

Name: sat_node/3	Module: dtmc_model_checking
Name: prob_calc_sub/5	Module: dtmc_model_checking
Name: prob_calc/5	Module: dtmc_model_checking
Name: prob_calc_sub/6	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: pre_process_formula/4	Module: dtmc_model_checking
Name: against/3	Module: dtmc_model_checking

Name: !
Name: table_prob0/3	dynamic predicate
Name: retract/1
Name: asserta/1
Name: RECURSIVE_CALL/4	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

Name: !
Name: table_prob1/3	dynamic predicate
Name: retract/1
Name: asserta/1
Name: RECURSIVE_CALL/4	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/3	dynamic predicate

Name: =/2
Name: find_prob_u/4	Module: dtmc_model_checking
Name: ->/3
Name: state/1	Module: dtmc_model_checking
Name: prob_calc_u1/5	Module: dtmc_model_checking
Name: retractall/1

Name: against/3	Module: dtmc_model_checking
Name: prob_current/2	dynamic predicate
Name: assert/1
Name: retract/1
Name: is/2
Name: sat/2	Module: dtmc_model_checking
Name: transition_probability/3	Module: dtmc_model_checking

Name: RECURSIVE_CALL/6	Module: dtmc_model_checking
Name: is/2
Name: sat/2	Module: dtmc_model_checking
Name: transition_probability/3	Module: dtmc_model_checking
Name: >/2
Name: against/3	Module: dtmc_model_checking
Name: prob_current/2	dynamic predicate
Name: assert/1
Name: retract/1
Name: ->/3

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

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

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

Name: pctl_model_check/4	Module: dtmc_model_checking
Name: sat_not/2	Module: dtmc_model_checking
Name: prob_calc/5	Module: dtmc_model_checking
Name: prob0/4	Module: dtmc_model_checking
Name: sat/1	Module: dtmc_model_checking
Name: prob_calc_sub/6	Module: dtmc_model_checking
Name: sat_g/2	Module: dtmc_model_checking
Name: prob1/4	Module: dtmc_model_checking
Name: prob_calc_sub/5	Module: dtmc_model_checking
Name: sat_gk/2	Module: dtmc_model_checking

Name: is/2
Name: RECURSIVE_CALL/2	Module: dtmc_model_checking
Name: =/2
Name: ->/3
Name: ground/1
Name: negate_operator/2	Module: dtmc_model_checking
Name: retractall/1
Name: sat_node/3	Module: dtmc_model_checking
Name: node/1	dynamic predicate
Name: assert/1
Name: retract/1
Name: sat_g/2	Module: dtmc_model_checking
Name: sat_gk/2	Module: dtmc_model_checking
Name: sat_not/2	Module: dtmc_model_checking
Name: \=/2
Name: check_ap/2	Module: foo_error
Name: fail

Name: sat_dynamic/3	Module: dtmc_model_checking
Name: =/2
Name: ->/3
Name: against/3	Module: dtmc_model_checking
Name: prob_calc/4	Module: dtmc_model_checking

Name: member/2
Name: find_initialised_states/1	Module: state_space

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

prob_prolog/extensions/markov/dtmc_model_checking.pl

Modules

Predicates of dtmc_model_checking

Module Information

Dynamic Predicates: node/1 prob_current/2 table_prob0/3 table_prob1/3

451 Lines

28 Predicates

8 Exports

12 Imports

Predicates:

Determinacy Checker: