162 Lines

10 Predicates

Imported Modules: module_information ordsets lists

2 Exports

4 specified Imports

Imports	Exports
Name: conjunct_predicates/2 Module: bsyntaxtree Name: conjunction_to_list/2 Module: bsyntaxtree Name: create_negation/2 Module: bsyntaxtree Name: create_implication/3 Module: bsyntaxtree	Name: down/4 Name: ctgDown/6

Imports

Exports

Name: conjunct_predicates/2

Module: bsyntaxtree

Name: conjunction_to_list/2

Module: bsyntaxtree

Name: create_negation/2

Module: bsyntaxtree

Name: create_implication/3

Module: bsyntaxtree

Name: down/4

Name: ctgDown/6

Predicates

Predicates:

ctgDown_aux_find_level/6

common_literals(Q1,Q2,CQ) :-
    conjunction_to_list(Q1,Q1L),
    conjunction_to_list(Q2,Q2L),
    list_to_ord_set(Q1L,Q1S),
    list_to_ord_set(Q2L,Q2S),
    ord_intersection(Q1S,Q2S,CQS),
    conjunct_predicates(CQS,CQ).

Calls:

Name: conjunct_predicates/2	Module: bsyntaxtree
Name: ord_intersection/3	Module: foo_error
Name: list_to_ord_set/2	Module: foo_error
Name: conjunction_to_list/2	Module: bsyntaxtree

Called:

Name: ctgDown_aux2/8	Module: mic_generation
Name: down_aux/3	Module: mic_generation

ctgDown/6

ctgDown(Cube,I,K,FramesIn,FramesOut,CubeOut) :-
% set current depth to 1
ctgDown(Cube,[],1,I,K,FramesIn,FramesOut,CubeOut).

Calls:

Name: ctgDown/8

Module: mic_generation

Called:

Name: ctgDown/6	Module: mic_generation
Name: ctgDown_aux2/8	Module: mic_generation

ctgDown/8

ctgDown([],Fixed,_,_,_,Frames,Frames,Fixed2) :- reverse(Fixed,Fixed2). % TODO: why do i need to reverse?!

ctgDown([C|Cs],Fixed,CurDepth,I,K,FramesIn,FramesOut,CubeOut) :-
    append(Cs,Fixed,FC),
    conjunct_predicates(FC,Q),
    (ctgDown_aux(Q,CurDepth,I,K,FramesIn,FramesT)
    -> ctgDown(Cs,Fixed,CurDepth,I,K,FramesT,FramesOut,CubeOut)
    ; ctgDown(Cs,[C|Fixed],CurDepth,I,K,FramesIn,FramesOut,CubeOut)).

Calls:

Name: RECURSIVE_CALL/8	Module: mic_generation
Name: ctgDown_aux/6	Module: mic_generation
Name: ->/3
Name: conjunct_predicates/2	Module: bsyntaxtree
Name: append/3
Name: reverse/2	Module: foo_error

Called:

Name: ctgDown/6	Module: mic_generation
Name: ctgDown_aux2/8	Module: mic_generation

ctgDown_aux/6

ctgDown_aux(Q,CurDepth,I,K,FramesIn,FramesOut) :-
% set current counter examples to generalization counter to 0
ctgDown_aux(Q,CurDepth,0,I,K,FramesIn,FramesOut).

Calls:

Name: ctgDown_aux/7

Module: mic_generation

Called:

Name: ctgDown/8	Module: mic_generation
Name: ctgDown_aux2/8	Module: mic_generation

ctgDown_aux/7

ctgDown_aux(Q,_Depth,_CTGs,_I,_K,Frames,Frames) :-
    % as in the simple down case
    % return false if I does not imply not q
    % i.e. if there is a solution for I & q
    initial_state(Q), !, fail.

ctgDown_aux(Q,_Depth,_CTGs,I,_K,Frames,Frames) :-
    % again this is equivalent to the simple case
    % return true if
    % F_i & not q & T => not q'
    create_negation(Q,NegQ),
    prime_predicate(Q,PrimedQ),
    in_solver_on_level(I,Frames,IS),
    conjunct_predicates([NegQ,PrimedQ|IS],Pred),
    solve(Pred,Result),
    Result = contradiction_found(_), !.

ctgDown_aux(_,Depth,_,_,_,Frames,Frames) :-
    % fail if Depth is too large (currently 2 - needs experiments)
    Depth > 2, !, fail.

ctgDown_aux(Q,Depth,CTGs,I,K,FramesIn,FramesOut) :-
    % with F_i ^ not q state
    in_solver_on_level(I,FramesIn,IS),
    create_negation(Q,NegQ),
    conjunct_predicates([NegQ|IS],Pred),
    solve(Pred,Result),
    Result = solution(F_iQState), !,
    create_state_predicate(F_iQState,F_iQStatePred),
    ctgDown_aux2(F_iQStatePred,Q,Depth,CTGs,I,K,FramesIn,FramesOut).

Calls:

Name: ctgDown_aux2/8	Module: mic_generation
Name: create_state_predicate/2	Module: foo_error
Name: !
Name: =/2
Name: solve/2	Module: foo_error
Name: conjunct_predicates/2	Module: bsyntaxtree
Name: create_negation/2	Module: bsyntaxtree
Name: in_solver_on_level/3	Module: foo_error
Name: fail
Name: >/2
Name: prime_predicate/2	Module: foo_error
Name: initial_state/1	Module: foo_error

Called:

Name: ctgDown/8	Module: mic_generation
Name: ctgDown_aux2/8	Module: mic_generation

ctgDown_aux2/8

ctgDown_aux2(S,Q,Depth,CTGs,I,K,FramesIn,FramesOut) :-
    % max ctgs currently 3 - needs experiments
    CTGs < 3, I > 0,

    % Init => not S
    get_initial_state_predicate(Init),
    conjunct_predicates([Init,S],IAndS),
    solve(IAndS,ResultIAndS),
    ResultIAndS = contradiction_found(_), !,

    % F_i-1 & not S & T => not s'
    create_negation(S,NegS),
    prime_predicate(S,SPrimed),
    IMinus1 is I - 1,
    in_solver_on_level(IMinus1,FramesIn,F_I),
    conjunct_predicates([NegS,SPrimed|F_I],Consecution),
    solve(Consecution,ResultConsecution),
    ResultConsecution = contradiction_found(_), !,

    % we found a new counterexample to generalization
    NCTGs is CTGs + 1,
    % TODO: for loop to find J
    create_negation(SPrimed,NegSPrimed),
    ctgDown_aux_find_level(I,K,NegS,NegSPrimed,FramesIn,J),
    JMinus1 is J - 1,
    Depth2 is Depth + 1,
    conjunction_to_list(S,SList),
    ctgDown(SList,[],Depth2,JMinus1,K,FramesIn,FramesT,SOut),
    % add modified not s to frames on level J and recur (while loop in paper)
    % instead of adding not s, we add the former conjuncts and use them as disjuncts
    add_clauses_to_level(J,FramesT,SOut,FramesTT),
    ctgDown_aux(Q,Depth,NCTGs,I,FramesTT,FramesOut).

ctgDown_aux2(S,Q,Depth,_CTGs,I,K,FramesIn,FramesOut) :-
    % the else branch
    common_literals(Q,S,NewQ),
    ctgDown_aux(NewQ,Depth,I,K,FramesIn,FramesOut).

Calls:

Name: ctgDown_aux/6	Module: mic_generation
Name: common_literals/3	Module: mic_generation
Name: add_clauses_to_level/4	Module: foo_error
Name: ctgDown/8	Module: mic_generation
Name: conjunction_to_list/2	Module: bsyntaxtree
Name: is/2
Name: ctgDown_aux_find_level/6	Module: mic_generation
Name: create_negation/2	Module: bsyntaxtree
Name: !
Name: =/2
Name: solve/2	Module: foo_error
Name: conjunct_predicates/2	Module: bsyntaxtree
Name: in_solver_on_level/3	Module: foo_error
Name: prime_predicate/2	Module: foo_error
Name: get_initial_state_predicate/1	Module: foo_error
Name: >/2
Name: </2

Called:

Name: ctgDown_aux/7

Module: mic_generation

ctgDown_aux_find_level/6

ctgDown_aux_find_level(K,K,_,_,_,K).

ctgDown_aux_find_level(I,_K,NegS,NegSPrimed,Frames,J) :-
    in_solver_on_level(I,Frames,F_I),
    conjunct_predicates([NegS|F_I],LHS),
    create_implication(LHS,NegSPrimed,Implies),
    solve(Implies,Result),
    Result = contradiction_found(_), !,
    J = I.

ctgDown_aux_find_level(I,K,NegSPrimed,SPrimed,Frames,J) :-
    I2 is I + 1,
    ctgDown_aux_find_level(I2,K,NegSPrimed,SPrimed,Frames,J).

Calls:

Name: RECURSIVE_CALL/6	Module: mic_generation
Name: is/2
Name: =/2
Name: !
Name: solve/2	Module: foo_error
Name: create_implication/3	Module: bsyntaxtree
Name: conjunct_predicates/2	Module: bsyntaxtree
Name: in_solver_on_level/3	Module: foo_error

Called:

Name: ctgDown_aux2/8

Module: mic_generation

down/4

down(Cube,I,Frames,CubeOut) :-
down(Cube,[],I,Frames,CubeOut).

Calls:

Name: down/5

Module: mic_generation

Called:

Name: down/4

Module: mic_generation

down/5

down([],Fixed,_,_,Fixed2) :- reverse(Fixed,Fixed2). % TODO: why do i need to reverse?!

down([C|Cs],Fixed,I,Frames,COut) :-
    append(Cs,Fixed,FC),
    conjunct_predicates(FC,Q),
    (down_aux(Q,I,Frames)
    -> down(Cs,Fixed,I,Frames,COut)
    ; down(Cs,[C|Fixed],I,Frames,COut)).

Calls:

Name: RECURSIVE_CALL/5	Module: mic_generation
Name: down_aux/3	Module: mic_generation
Name: ->/3
Name: conjunct_predicates/2	Module: bsyntaxtree
Name: append/3
Name: reverse/2	Module: foo_error

Called:

Name: down/4

Module: mic_generation

down_aux/3

down_aux(Q,_I,_Frames) :-
    % return false if I does not imply not q
    % i.e. if there is a solution for I & q
    initial_state(Q), !, fail.

down_aux(Q,I,Frames) :-
    % F_i & not q & T => not q'
    create_negation(Q,NegQ),
    prime_predicate(Q,PrimedQ),
    in_solver_on_level(I,Frames,IS),
    get_transition_predicate(T),
    conjunct_predicates([NegQ,PrimedQ,T|IS],Pred),
    solve(Pred,Result),
    Result = contradiction_found(_), !.

down_aux(Q,I,Frames) :-
    % with F_i ^ not q state
    in_solver_on_level(I,Frames,IS),
    create_negation(Q,NegQ),
    get_transition_predicate(T),
    conjunct_predicates([NegQ,T|IS],Pred),
    solve(Pred,Result),
    Result = solution(F_iQState), !,
    create_state_predicate(F_iQState,F_iQStatePred),
    common_literals(Q,F_iQStatePred,NewQ),
    down_aux(NewQ,I,Frames).

Calls:

Name: RECURSIVE_CALL/3	Module: mic_generation
Name: common_literals/3	Module: mic_generation
Name: create_state_predicate/2	Module: foo_error
Name: !
Name: =/2
Name: solve/2	Module: foo_error
Name: conjunct_predicates/2	Module: bsyntaxtree
Name: get_transition_predicate/1	Module: foo_error
Name: create_negation/2	Module: bsyntaxtree
Name: in_solver_on_level/3	Module: foo_error
Name: prime_predicate/2	Module: foo_error
Name: fail
Name: initial_state/1	Module: foo_error

Called:

Name: down/5

Module: mic_generation

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),_3441,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/symbolic_model_checker/mic_generation.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bsyntaxtree) does not exist
! goal: absolute_file_name(probsrc(bsyntaxtree),_261,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/symbolic_model_checker/mic_generation.pl')])

mic_generation

prob_prolog/src/symbolic_model_checker/mic_generation.pl

Modules

Predicates of mic_generation

Module Information

162 Lines

10 Predicates

Imported Modules: module_information ordsets lists

2 Exports

4 specified Imports

Predicates:

common_literals/3

ctgDown/6

ctgDown/8

ctgDown_aux/6

ctgDown_aux/7

ctgDown_aux2/8

ctgDown_aux_find_level/6

down/4

down/5

down_aux/3

Determinacy Checker: