Dynamic Predicates: assertion_state/1 assertion_task/2 callback_load/2 count/1 state/2 trans/3 debug_mode/0

265 Lines

20 Predicates

Imported Modules: lists process module_information process translate

2 Exports

21 specified Imports

Imports	Exports
Name: fast_buf_read/2 Module: fastrw Name: fast_buf_write/3 Module: fastrw Name: add_error/3 Module: error_manager Name: init_zmq/0 Module: zmq/zmq Name: setup_worker/5 Module: zmq/zmq Name: work_reactor/1 Module: zmq/zmq Name: teardown_worker/0 Module: zmq/zmq Name: new_results_message/1 Module: zmq/zmq Name: start_timer/0 Module: zmq/zmq Name: stop_timer/0 Module: zmq/zmq Name: msg_put_str/2 Module: zmq/zmq Name: put_succ/4 Module: zmq/zmq Name: add_stats/1 Module: zmq/zmq Name: send_and_destroy_msg/1 Module: zmq/zmq Name: state_corresponds_to_initialised_b_machine/2 Module: specfile Name: b_test_boolean_expression_for_ground_state/5 Module: b_interpreter Name: b_get_machine_searchscope/1 Module: bmachine Name: test_boolean_expression_in_node/2 Module: eclipse_interface Name: create_negation/2 Module: bsyntaxtree Name: depth_breadth_first_mode/1 Module: state_space_exploration_modes Name: print_dynamic_pred/3 Module: tools_printing	Name: start_worker/5 Name: load/1

Imports

Exports

Name: fast_buf_read/2

Module: fastrw

Name: fast_buf_write/3

Module: fastrw

Name: add_error/3

Module: error_manager

Name: init_zmq/0

Module: zmq/zmq

Name: setup_worker/5

Module: zmq/zmq

Name: work_reactor/1

Module: zmq/zmq

Name: teardown_worker/0

Module: zmq/zmq

Name: new_results_message/1

Module: zmq/zmq

Name: start_timer/0

Module: zmq/zmq

Name: stop_timer/0

Module: zmq/zmq

Name: msg_put_str/2

Module: zmq/zmq

Name: put_succ/4

Module: zmq/zmq

Name: add_stats/1

Module: zmq/zmq

Name: send_and_destroy_msg/1

Module: zmq/zmq

Name: state_corresponds_to_initialised_b_machine/2

Module: specfile

Name: b_test_boolean_expression_for_ground_state/5

Module: b_interpreter

Name: b_get_machine_searchscope/1

Module: bmachine

Name: test_boolean_expression_in_node/2

Module: eclipse_interface

Name: create_negation/2

Module: bsyntaxtree

Name: depth_breadth_first_mode/1

Module: state_space_exploration_modes

Name: print_dynamic_pred/3

Module: tools_printing

Name: start_worker/5

Name: load/1

Dynamic: true

mk_assertion_violation/2

process(assertion,result([], []), S) :- findall(check(N),assertion_task(N,_),S).

process(check(N),R,[]) :- %process_id(PID),
    assertion_task(N,A),
    check_assertion(A,R).

process(root,R,S) :- process(state(root),R,S).

process(state(State),result(ResString, StateAtom),Successors) :- !, % print(treating(State)),nl,flush_output,
    % statistics(walltime,[T1,_]),
    % statistics(runtime,[T3,_]),
    % current_prolog_flag(gc,G),print(gc(G)),nl,
    specfile:prepare_state_for_specfile_trans(State,root,PreparedState), % will perform unpacking of constants just once, for example
    % pass root as stateid, we have no reference state id available here (mainly used for operation caching)
    (debug_mode->count(X),assertz(state(X,State)),inc;true),
    (state_corresponds_to_initialised_b_machine(PreparedState,S2) ->
    bmachine:b_get_invariant_from_machine(Invariant), % TO DO: get unproven invariant if this is not the initial state
    ( b_test_boolean_expression_for_ground_state(Invariant,[],S2,'ParB worker',0)
    % TO DO: add time_out, specialized invariants, assertions, ...
    -> ResString = [] %, print(invariant_ok),nl
    ; ResString = ['invariant_violated'], translate:translate_bstate(State, StateAtom)
    )
    % ,print(checked_inv(Res)),nl
    ; ResString = [] %, print(not_initialised(PreparedState)),nl
    ),

    findall(state(NewState),
    compute_successors(PreparedState,_ActionName,NewState),
    S),
    (debug_mode->dump_trans(PreparedState);true),
    % print(successors(S)),nl,
    %statistics(walltime,[T2,_]),
    %statistics(runtime,[T4,_]),
    %TW is T2 - T1,
    %TR is T4 - T3,

    %(TW > 10 -> ( print(time(TW,TR)),nl,statistics,print(x),nl);true),
    Successors = S.

process(max_reached,Res,[]) :- !,
    (succeed_max:max_reached -> Res=true ; Res=false).

process(X,_,S) :- print(unhandled(X)),nl, S=[].

Meta: start_worker(+,+,+,+,1)

zmq_check/3

Determinacy Checker

Determinacy Checker:

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

Name: translate_bstate/2	Module: translate
Name: mk_assertion_violation/2	Module: worker
Name: =/2
Name: b_test_boolean_expression_for_ground_state/5	Module: b_interpreter
Name: ->/3
Name: assertion_state/1	dynamic predicate

Name: is_not_interesting/1	Module: worker
Name: not/1
Name: specfile_trans/6	Module: specfile
Name: specfile_possible_trans_name/2	Module: specfile

Name: process/3	Module: worker
Name: inc/0	Module: worker

Name: print_dynamic_pred/3	Module: tools_printing
Name: nl
Name: print/1
Name: portray_clause/1
Name: true
Name: max_reached/0	Module: succeed_max
Name: ->/3

Name: assertz/1
Name: is/2
Name: retractall/1
Name: count/1	Module: worker

worker

prob_prolog/extensions/zmq/worker/worker.pl

Modules

Predicates of worker

Module Information

Dynamic Predicates: assertion_state/1 assertion_task/2 callback_load/2 count/1 state/2 trans/3 debug_mode/0

265 Lines

20 Predicates

Imported Modules: lists process module_information process translate

2 Exports

21 specified Imports

Predicates:

check_assertion/2

compute_successors/3

count/1

dump/0

dump_trans/1

dump_trans/2

inc/0

is_not_interesting/1

load/1

mk_assertion_violation/2

my_reactor_loop/0

print_stats/1

print_substat/1

process/3

put_results/2

put_results2/2

put_successors/3

set_debug/0

start_worker/5

zmq_check/3

Determinacy Checker:

Name: fail
Name: add_error/3	Module: error_manager
Name: true
Name: call/2
Name: if/3
Name: callback_load/2	dynamic predicate
Name: fast_buf_read/2	Module: fastrw

Name: RECURSIVE_CALL/0	Module: worker
Name: flush_output
Name: nl
Name: print/1
Name: =\=/2
Name: ->/3
Name: !
Name: work_reactor/1	Module: zmq/zmq

Name: put_results2/2	Module: worker
Name: zmq_check/3	Module: worker

Name: put_results/2	Module: worker
Name: msg_put_str/2	Module: zmq/zmq

Name: RECURSIVE_CALL/3	Module: worker
Name: put_succ/4	Module: zmq/zmq
Name: fast_buf_write/3	Module: fastrw

Name: teardown_worker	Module: zmq/zmq
Name: my_reactor_loop/0	Module: worker
Name: !
Name: setup_worker/5	Module: zmq/zmq
Name: depth_breadth_first_mode/1	Module: state_space_exploration_modes
Name: assertz/1
Name: retractall/1
Name: init_zmq	Module: zmq/zmq