ample_sets

action_does_not_modify_inv_or_inv_cannot_be_repaired(_Vars,[]).

action_does_not_modify_inv_or_inv_cannot_be_repaired(Vars,[Conj|Conjs]) :-
    find_identifier_uses(Conj,[],UsedIds),
    ord_intersection(UsedIds,Vars,Common),
    (Common=[]
    -> true % invariant not affected by action
    ; ord_seteq(Common,UsedIds) % we write all variables of an invariant; no independent action can change/repair its status
    ),
    action_does_not_modify_inv_or_inv_cannot_be_repaired(Vars,Conjs).

add_action_name_transitions([],_CurID,_ActionName,RemTransitions,RemTransitions,no,ActSuccsGen,ActSuccsGen).

add_action_name_transitions([(ActionName1,Transitions)|R],CurID,ActionName,IgnoredActions_so_far,
    RemTransitions,FullyExplored,ActSuccsGen,ActSuccs) :-
    (ActionName == ActionName1 ->
    % in this case we do not need to go through the rest of the transitions list
    add_action_transitions(ActionName,Transitions,CurID,NewIds),
    ActSuccsGen1 = [(ActionName,NewIds)|ActSuccsGen],
    append(IgnoredActions_so_far,R,AllRemainedActions),
    (cycle_condition_check_positive_l(NewIds) ->
    debug_println(9,'*********** POSSIBLE CYCLE DETECTED *************'),
    debug_println(9,computing_all_other_enabled_actions(back_transition(ActionName),AllRemainedActions)),
    add_all_other_enabled_transitions(AllRemainedActions,CurID,ActSuccsGen1,ActSuccs),
    RemTransitions=[],
    FullyExplored = yes
    ; FullyExplored = no, RemTransitions = AllRemainedActions, ActSuccs=ActSuccsGen1)
    ;
    % keeping track of all ignored actions so far, we don't want to go through the same order of actions every time we
    % want to add a transition from AmpleSet to the state space
    ord_add_element(IgnoredActions_so_far, (ActionName1,Transitions), IgnoredActions_so_far1),
    add_action_name_transitions(R,CurID,ActionName,IgnoredActions_so_far1,RemTransitions,FullyExplored,ActSuccsGen,ActSuccs)
).

add_action_transitions(_ActionName,Transitions,CurID,NewIds) :-
    findall(NewId,
    (member((Act,NewExpression,TransInfo,Residue),Transitions),
    tcltk_interface: add_trans_id_with_infos(CurID,[],Act,NewExpression,Residue,NewId,TransInfo,_)),NewIds).

add_all_other_enabled_transitions([],_CurID,ActSuccsGen,ActSuccsGen).

add_all_other_enabled_transitions([(ActionName,Transitions)|R],CurID,ActSuccsGen,ActSuccs) :-
    add_action_transitions(ActionName,Transitions,CurID,NewIds),
    ActSuccsGen1 = [(ActionName,NewIds)|ActSuccsGen],
    add_all_other_enabled_transitions(R,CurID,ActSuccsGen1,ActSuccs).

add_transitions(AmpleSet,CurID,Transitions,ActNameSuccessors) :-
    add_transitions(no,AmpleSet,CurID,Transitions,[],ActNameSuccessors).

add_transitions(yes,_AmpleSet,_CurID,_Transitions,ActNameSuccessors,ActNameSuccessors).

add_transitions(_FullyExplored,[],_CurID,_Transitions,ActNameSuccessors,ActNameSuccessors).

add_transitions(no,[ActionName|ActNames],CurID,Transitions,ActNameSuccessorsGen,ActNameSuccessors) :-
    add_action_name_transitions(Transitions,CurID,ActionName,[],RemTransitions,FullyExplored,ActNameSuccessorsGen,ActNameSuccessorsGen1),
    add_transitions(FullyExplored,ActNames,CurID,RemTransitions,ActNameSuccessorsGen1,ActNameSuccessors).

can_enable_certain_action(Act,ActionToBeEnabled,CurID) :-
    ( enables(Act,ActionToBeEnabled) ->
    debug_println(9,enables(Act,ActionToBeEnabled))
    ;
    enable_graph(EnableGraph),
    min_path(Act,ActionToBeEnabled,EnableGraph,P,L),
    debug_print_path(CurID,P,L),
    assertz(enables(Act,ActionToBeEnabled))).

check_cycle_proviso(AmpleSet) :-
    % in case that we don't check for invariant violations, we don't have to prove the stuttering condition for AmpleSet
    (check_cycle_proviso % true when we search for invariant violations
    -> stutter_actions(AmpleSet)
    ; true).

check_enable_dependency(Act,Act1,Pred,CurID) :-
    debug_println(9,checking_guard_dependency(Act,Act1,Pred)),
    visited_expression(CurID,RawState),
    state_corresponds_to_initialised_b_machine(RawState,State),
    empty_state(LocalState),
    % if the enable predicate Pred evaluates to false we know that (Act,Act1) is a dependent pair
    \+ b_interpreter:b_test_boolean_expression_cs(Pred,LocalState,State,'enable dependency',Act:Act1).

check_enabling_path(CurID,Act,DisabledActions,AmpleSet,EnableGraph,Depth) :-
    findall(DepDisAct,(member(DepDisAct,DisabledActions),depends_on_ample_set_and_coenabled(DepDisAct,AmpleSet,_Act)),DependentDisabledActions),
    ( DependentDisabledActions = [] ->
    fail % in this case we know that no action dependent on AmpleSet can be enabled after executing Act
    ;
    enables_pred_action1(Act,DependentDisabledActions,AmpleSet,CurID,EnableGraph,Depth)).

check_if_action_is_stutter_wrt_inv(Act) :- %print(check_stutter(Act)),nl,
    b_operation_preserves_full_invariant(Act),!,
    assertz(stutter_action(Act)),
    debug_println(19,stutter_according_to_proof_info(Act)).

check_if_action_is_stutter_wrt_inv(Act) :-
    b_specialized_invariant_for_op(Act,Invariant), %translate:print_bexpr(Invariant),nl,
    conjunction_to_list(Invariant,Conjunctions), % getting all conjunctions from the invariant
    b_get_read_write(Act,_Reads,Writes), % print(writes(Act,Writes)),nl,
    ( action_does_not_modify_inv_or_inv_cannot_be_repaired(Writes,Conjunctions)
    -> assertz(stutter_action(Act)),
    print(stutter_or_not_repairable(Act)),nl,
    debug_println(19,stutter_or_not_repairable(Act))
    ; assertz(visible_action(Act)),fail
).

check_if_enabled(CurID,Act,DisAct,AmpleSet,EnableGraph) :-
    min_path(Act,DisAct,EnableGraph,P,L),
    sets_disjoint(AmpleSet,P),
    debug_print_path(CurID,P,L),
    assertz(enables(Act,DisAct)).

check_stutter_condition(AmpleSet,AllEnabledActions) :-
    \+ ord_seteq(AmpleSet,AllEnabledActions),!,
    check_cycle_proviso(AmpleSet).

clear_dynamic_predicates_for_POR :-
    reset_static_dynamic_predicates_POR,
    reset_runtime_dynamic_predicates_POR.

compute_ample_actions(CurID,AllEnabledActions,POROptions,AmpleSet) :-
    % get_ample_actions/5 call only reasonable to be executed when more than one actions are enabled in CurID
    (more_than_one_event(AllEnabledActions) ->
    get_ample_actions(CurID,AllEnabledActions,POROptions,AmpleSet)
    ;
    AmpleSet = AllEnabledActions
).

compute_ample_set2(CurID,CurState,por(TYPE,UseEnableGraph,Depth,PGE)) :-
    reset_max_reached,
    prepare_state_for_specfile_trans(CurState,CurID,PreparedCurState),
    get_enabled_actions_at_state(CurID,PreparedCurState,PGE,TopLevelActions,Transitions,DisabledTopLevelActions),
    % we want only unique action names for analyzing and computing of ample sets
    list_to_ord_set(TopLevelActions,TopLevelActionsSet),
    % compute a sound ample set from all actions enabled in state CurID
    compute_ample_actions(CurID,TopLevelActionsSet,por(TYPE,UseEnableGraph,Depth,PGE),AmpleSet),
    debug_println(20,sets(CurID,allActions(TopLevelActionsSet),ampleSet(AmpleSet))),
    % mark state as visited (Cycle Condition (A 4))
    assertz(explored_state(CurID)),
    ( AmpleSet \= [] ->
    % compute just the actions from the ample set (case of state space reduction)
    % AmpleSet is a non-empty subset of enabled(CurID), AmpleSet can be equal to AllEnabledActions
    add_transitions(AmpleSet,CurID,Transitions,ActNameSuccessors),
    update_enabled_disabled_information_if_necessary(PGE,ActNameSuccessors,DisabledTopLevelActions,AmpleSet)
    ;
    true /* DEADLOCK */
    ),
    (max_reached ->
    assert_max_reached_for_node(CurID),
    MaxReached=true
    ; MaxReached=false
    ),
    (CurID==root ->
    save_constants(MaxReached)
    ; add_new_transitions_to_cache(CurID)
    ),!. % once we have computed the ample set in CurState we don't want to backtrack

compute_closure_set([],_CurID,ClosureSet,_AllEnabledActions,ClosureSet).

compute_closure_set([Act|Acts],CurID,ClosureSet,AllEnabledActions,Result) :-
    ord_add_element(ClosureSet,Act,ClosureSet1),
    get_new_work_set(Act,Acts,CurID,AllEnabledActions,ClosureSet1,NewWorkSet),
    compute_closure_set(NewWorkSet,CurID,ClosureSet1,AllEnabledActions,Result).

cycle_condition_check_positive_l(NewIds) :-
    check_cycle_proviso,!,
    member(NewId,NewIds),
    nonvar(NewId),
    explored_state(NewId).

debug_print_path(CurID,Path,Length) :-
    debug_println(20,'***** Enable Path *****'),
    debug_println(20,path(CurID,Path,Length)),
    debug_println(20,'***********************').

depends_on_ample_set_and_coenabled(Act,AmpleSet,Act1) :-
    member(Act1,AmpleSet),
    dependent_act(Act,Act1,_Status,Coenabled),
    Coenabled==true.

enables_action(CurID,Act,DisAct,AmpleSet,EnableGraph) :-
    ( enables(Act,DisAct) ->
    % should improve performance a little bit (not applicable when using enable graphs)
    debug_println(9,enables(Act,DisAct))
    ; check_if_enabled(CurID,Act,DisAct,AmpleSet,EnableGraph) ->
    true
    ;
    fail
).

enables_pred_action1(Act,DepDisActs,AmpleSet,CurID,EnableGraph,Depth) :-
    % visited_expression/2 and state_corresponds_to_initialised_b_machine/2 should be called once for each state,
    % avoid multiple calls per state
    (Depth==0 ->
    empty_state(ST)
    ;
    visited_expression(CurID,RawState),
    state_corresponds_to_initialised_b_machine(RawState,ST)
    ),
    %Pred =.. [evaluate_enabling_predicate_for_por, ST, AmpleSet],
    enable_graph: path_set(EnableGraph,Act,DepDisActs,enable_graph,
    evaluate_enabling_predicate_for_por(ST,AmpleSet),Depth,Path,Length),
    debug_print_path(CurID,Path,Length).

find_enabling_action(Act,CurID,AllEnabledActions,ClosureSet,Act1) :-
    member(Act1,AllEnabledActions),
    ord_nonmember(Act1,ClosureSet),
    can_enable_certain_action(Act1,Act,CurID).

get_ample_actions(CurID,AllEnabledActions,POROptions,AmpleSet) :-
    get_preference(por_heur,Pref),
    get_ample_actions_pref(Pref,CurID,AllEnabledActions,POROptions,AmpleSet).

get_ample_actions_pref(minimal,CurID,AllEnabledActions,POROptions,AmpleSet) :- !,
    get_possible_ample_actions_minimal(AllEnabledActions,CurID,AllEnabledActions,POROptions,AmpleSet).

get_ample_actions_pref(Pref,CurID,AllEnabledActions,POROptions,AmpleSet) :-
    get_possible_ample_actions(Pref,AllEnabledActions,CurID,AllEnabledActions,POROptions,AmpleSet).

get_dependency_set(Act,AllEnabledActions,CurID,DepActions_so_far) :-
    vertices_edges_to_ugraph([],[],G),
    get_dependency_tuples_converted_to_edges(Act,AllEnabledActions,RestEnabledActions,CurID,Edges),
    add_edges(G,Edges,G1),
    get_dependency_set1(Act,G1,[],RestEnabledActions,CurID,DepActions_so_far).

get_dependency_set1(Act,G,G,_Actions,_CurID,Res) :-
    reachable(Act,G,Res).

get_dependency_set1(Act,G,_GPrime,Actions,CurID,Res) :-
    GPrime1 = G,
    vertices(G,Vertices),
    findall([V-Act1,Act1-V],(member(Act1,Actions),member(V,Vertices),is_dependent_to(V,Act1,CurID)),NewEdges),
    append(NewEdges,NewEdges1),
    add_edges(G,NewEdges1,G1),vertices(G1,Vertices1),
    ord_subtract(Actions,Vertices1,Actions1),
    get_dependency_set1(Act,G1,GPrime1,Actions1,CurID,Res).

get_dependency_set_closure(Act,WorkSet,CurID,ClosureSet1,NewWorkSet) :-
    findall(Act1,(is_dependent_to_and_coenabled(Act,Act1,CurID),ord_nonmember(Act1,ClosureSet1)),NewActions),
    list_to_ord_set(NewActions,NewActionsSet),
    ord_union(WorkSet,NewActionsSet,NewWorkSet).

get_dependency_tuples_converted_to_edges(Act,AllEnabledActions,RestEnabledActions,CurID,Res) :-
    findall(Act1,(member(Act1,AllEnabledActions), is_dependent_to(Act,Act1,CurID)),DepActs),
    findall([Act-Act1,Act1-Act],member(Act1,DepActs),Edges),
    ord_subtract(AllEnabledActions,DepActs,RestEnabledActions),
    append(Edges,Res).

get_dependent_actions(CurID,_POROptions,Act,AllEnabledActions,DepActs,IndActions) :-
    % finding all dependent actions to Act (A 2.1)
    get_dependency_set(Act,AllEnabledActions,CurID,DepActs),
    ord_subtract(AllEnabledActions,DepActs,IndActions).

get_enabled_actions_at_state(CurID,CurState,PGE,EnabledTopLevelActions,Transitions,DisabledTopLevelActions) :-
    get_specfile_possible_trans_names(CurID,CurState,PGE,TopLevelActions,DisabledOperations),
    get_enabled_actions_at_state_aux(TopLevelActions,CurID,CurState,EnabledTopLevelActions,Transitions,DisabledOperationsNew),
    list_to_ord_set(DisabledOperationsNew,DisabledOperationsNewSet),
    ord_union(DisabledOperations,DisabledOperationsNewSet,DisabledTopLevelActions).

get_enabled_actions_at_state_aux(TopLevelActions,CurID,CurState,EnabledTopLevelActions,Transitions,DisabledTopLevelActionsNew) :-
    get_enabled_actions_at_state_aux2(TopLevelActions,CurID,CurState,[],EnabledTopLevelActions,[],Transitions,[],DisabledTopLevelActionsNew).

get_enabled_actions_at_state_aux2([],_CurID,_CurState,EnabledTopLevelActions,EnabledTopLevelActions,Transitions,Transitions,DisabledNew,DisabledNew).

get_enabled_actions_at_state_aux2([TopLevelAction|R],CurID,CurState,EnabledTopLevelActionsGen,EnabledTopLevelActions,TransitionsGen,Transitions,DisabledNewGen,DisabledNew) :-
    (get_top_level_action_transitions(CurID,CurState,TopLevelAction,ActionTransitionsTuple) ->
    EnabledTopLevelActionsGen1 = [TopLevelAction|EnabledTopLevelActionsGen],
    TransitionsGen1 = [ActionTransitionsTuple|TransitionsGen],
    DisabledNewGen1 = DisabledNewGen
    ;
    EnabledTopLevelActionsGen1 = EnabledTopLevelActionsGen,
    TransitionsGen1 = TransitionsGen,
    DisabledNewGen1 = [TopLevelAction|DisabledNewGen]
    ),
    get_enabled_actions_at_state_aux2(R,CurID,CurState,EnabledTopLevelActionsGen1,EnabledTopLevelActions,TransitionsGen1,Transitions,DisabledNewGen1,DisabledNew).

get_enabling_set_for_act(Act,WorkSet,CurID,AllEnabledActions,ClosureSet1,NewWorkSet) :-
    % Act is disabled at current state
    findall(Act1,find_enabling_action(Act,CurID,AllEnabledActions,ClosureSet1,Act1),NewActions),
    list_to_ord_set(NewActions,NewActionsSet),
    ord_union(WorkSet,NewActionsSet,NewWorkSet).

get_minimal_set([AmpleSet|Rest],MinAmpleSet) :-
    length(AmpleSet,Length),
    get_minimal_set_length(Length,AmpleSet,Rest,MinAmpleSet).

get_minimal_set_length(1,AmpleSet,_Rest,AmpleSet).

get_minimal_set_length(_Length,AmpleSet,[],AmpleSet).

get_minimal_set_length(Length,AmpleSet,[AmpleSet2|Rest],MinAmpleSet) :-
    length(AmpleSet2,Length2),
    (Length2<Length ->
    get_minimal_set_length(Length2,AmpleSet2,Rest,MinAmpleSet)
    ;
    get_minimal_set_length(Length,AmpleSet,Rest,MinAmpleSet)).

get_new_work_set(Act,WorkSet,CurID,AllEnabledActions,ClosureSet1,NewWorkSet) :-
    ord_member(Act,AllEnabledActions),!,
    get_dependency_set_closure(Act,WorkSet,CurID,ClosureSet1,NewWorkSet).

get_new_work_set(Act,WorkSet,CurID,AllEnabledActions,ClosureSet1,NewWorkSet) :-
    get_enabling_set_for_act(Act,WorkSet,CurID,AllEnabledActions,ClosureSet1,NewWorkSet).

get_possible_ample_actions(_Pref,[],_CurID,AllEnabledActions,_POROptions,AllEnabledActions).

get_possible_ample_actions(Pref,Actions,CurID,AllEnabledActions,POROptions,AmpleSet) :-
    % choosing of action for computing a possible ample set for CurID should be random
    select_enabled_action_pref(Pref,Actions,Act,RemainedActions),
    (get_valid_ample_set_act(CurID,POROptions,Act,AllEnabledActions,AmpleSet) -> % get ample set satisfying (A 2) and (A 3) i.r.t. Act
    true
    ; % search for another valid ample set
    get_possible_ample_actions(Pref,RemainedActions,CurID,AllEnabledActions,POROptions,AmpleSet)
).

get_possible_ample_actions_minimal(AllEnabledActions,CurID,AllEnabledActions,POROptions,AmpleSet) :-
    maplist(get_valid_ample_set_act_nonfail(CurID,AllEnabledActions,POROptions),AllEnabledActions,AmpleSets),
    get_minimal_set(AmpleSets,AmpleSet),
    debug_println(9,minimal_ample_set(AmpleSet,AmpleSets)).

get_possible_ample_set_closure(CurID,Act,AllEnabledActions,AmpleSet) :-
    get_valid_ample_set_act_closure(CurID,Act,AllEnabledActions,AmpleSet),!,
    check_stutter_condition(AmpleSet,AllEnabledActions). % checking (A 3)

get_specfile_possible_trans_names(CurState,TopLevelActions) :-
    findall(ActionName,specfile_possible_trans_name_for_successors(CurState,ActionName),TopLevelActions).

get_specfile_possible_trans_names(CurID,CurState,PGE,TopLevelActions,DisabledOperations) :-
    ( PGE\= off ->
    % get enabled top level actoions using the information from the PGE algo
    pge_algo: get_possible_enabled_trans_names(CurID,CurState,DisabledOperations,_EnabledOperations,TopLevelActions)
    ;
    get_specfile_possible_trans_names(CurState,TopLevelActions),
    DisabledOperations = [] % in case PGE is not on we don't have any information about the disabledness of actions
).

get_top_level_action_transitions(CurID,CurState,TopLevelAction,ActionTransitionsTuple) :-
    findall((Act,NewExpression,TransInf,Residue),
    specfile_trans_timeout(CurID,CurState,TopLevelAction,Act,NewExpression,TransInf,Residue),
    Transitions),
    % in case TopLevelAction is not enabled we do not save the transitions in the list
    Transitions\=[],
    ActionTransitionsTuple = (TopLevelAction,Transitions).

get_valid_ample_set_act(CurID,POROptions,Act,AllEnabledActions,AmpleSet) :-
    POROptions = por(ample_sets2,_,_,_),!,
    %% trying to find an ample set by the closure method
    get_possible_ample_set_closure(CurID,Act,AllEnabledActions,AmpleSet).

get_valid_ample_set_act(CurID,POROptions,Act,AllEnabledActions,AmpleSet) :-
    get_valid_ample_set_act_normal(CurID,POROptions,Act,AllEnabledActions,AmpleSet).

get_valid_ample_set_act_closure(CurID,Act,AllEnabledActions,AmpleSet) :-
    %(length(AllEnabledActions,3) -> trace;true),
    list_to_ord_set([Act],WorkSet),
    list_to_ord_set([],ClosureSet),
    compute_closure_set(WorkSet,CurID,ClosureSet,AllEnabledActions,Result),
    ord_intersection(Result,AllEnabledActions,AmpleSet).

get_valid_ample_set_act_nonfail(CurID,AllEnabledActions,POROptions,Act,AmpleSet) :-
    (get_valid_ample_set_act(CurID,POROptions,Act,AllEnabledActions,AmpleSet)
    -> true
    ; AmpleSet = AllEnabledActions).

get_valid_ample_set_act_normal(CurID,POROptions,Act,AllEnabledActions,AmpleSet) :-
    % finding a set (DepActs) satisfying (A 2.1) // there is only one possible set, do not recall here
    get_dependent_actions(CurID,POROptions,Act,AllEnabledActions,DepActs,IndActs),!,
    ( (is_enabling_dependency_condition_satisfied(IndActs,DepActs,AllEnabledActions,CurID,POROptions), % check whether DepActs satisfies (A 2.2)
    check_stutter_condition(DepActs,AllEnabledActions)) % checking (A 3)
    -> AmpleSet = DepActs
    ; fail). % should fail in order to try to get another valid ample set

is_dependent_to(Act,Act1,CurID) :-
    (dependent_act(Act,Act1,Status,_Coenabled) ->
    (Status=predicate(Pred) -> check_enable_dependency(Act,Act1,Pred,CurID); true)
    ;
    fail
).

is_dependent_to_and_coenabled(Act,Act1,CurID) :-
    dependent_act(Act,Act1,Status,true),
    (Status=predicate(Pred) -> check_enable_dependency(Act,Act1,Pred,CurID); true).

is_enabling_dependency_condition_satisfied([],_DepActs,_AllEnabledActions,_CurID,_POROptions) :- !,fail.

is_enabling_dependency_condition_satisfied(IndActs,DepActs,AllEnabledActions,CurID,POROptions) :-
    enable_graph(EnableGraph),
    vertices(EnableGraph,Vertices), % getting all possible actions that can be enabled
    % DisabledActions = Vertices\AllEnabledActions
    ord_subtract(Vertices,AllEnabledActions,DisabledActions),
    % searching for an independent action to Act that could enable a currently disabled action that is dependent to Act (A 2.2)
    \+may_enable_dep_action_list(IndActs,DepActs,DisabledActions,EnableGraph,CurID,POROptions).

is_stutter_action(Act) :-
    ( stutter_action(Act) ->
    debug_println(19,stutter_action(Act))
    ; visible_action(Act) ->
    debug_println(19,visible_action(Act)),
    fail
    ;
    check_if_action_is_stutter_wrt_inv(Act)
).

may_enable_dep_action(Act,AmpleSet,DisabledActions,EnableGraph,CurID,por(_TYPE,UseEnableGraph,Depth,_PGE)) :-
    ( UseEnableGraph = true ->
    check_enabling_path(CurID,Act,DisabledActions,AmpleSet,EnableGraph,Depth)
    ;
    member(DisAct,DisabledActions),
    % we check here only currently disabled actions dependent on AmpleSet that can be enabled later
    depends_on_ample_set_and_coenabled(DisAct,AmpleSet,_DepAct),
    % is there a path that can enable Act1, which is dependent on Act
    enables_action(CurID,Act,DisAct,AmpleSet,EnableGraph)
    ),
    !.

may_enable_dep_action_list(IndActs,DepActs,DisabledActions,EnableGraph,CurID,POROptions) :-
    member(Act2,IndActs),
    may_enable_dep_action(Act2,DepActs,DisabledActions,EnableGraph,CurID,POROptions).

more_than_one_event(SetOfActions) :-
    length(SetOfActions,L),L>1.

reset_runtime_dynamic_predicates_POR :-
    retractall(stutter_action(_)),
    retractall(visible_action(_)),
    retractall(explored_state(_)),
    retractall(enables(_,_)),
    retractall(check_cycle_proviso). % used to not track in the enable graph

reset_static_dynamic_predicates_POR :-
    retractall(dependent_act(_,_,_,_)),
    retractall(enable_graph(_)).

select_enabled_action_pref(random,Actions,Act,RemainedActions):- !,
    random_select(Act,Actions,RemainedActions).

select_enabled_action_pref(first,[Act|RemainedActions],Act,RemainedActions):- !.

select_enabled_action_pref(Pref,Actions,Act,RemainedActions) :-
    add_warning(ample_sets,'Unknown preference for choosing an action from the set of enabled actions: ', Pref),
    random_select(Act,Actions,RemainedActions). % choose the default option for choosing an action

sets_disjoint(AmpleSet,Path) :-
    list_to_ord_set(Path,OrdSet),
    \+ord_intersection(AmpleSet,OrdSet).

specfile_trans_timeout(CurID,CurState,ActionName,Act,NewExpression,TransInf,Residue) :-
    (use_no_timeout(CurID) ->
    specfile_trans(CurState,ActionName,Act,NewExpression,TransInf,Residue)
    ; preferences:preference(time_out,CurTO),
    time_out_with_enum_warning_for_findall(specfile_trans(CurState,ActionName,Act,NewExpression,TransInf,Residue),CurTO,TimeOutRes),
    pge_algo: check_timeout_result(CurID,ActionName,CurTO,TimeOutRes),
    Residue==[]
).

stutter_actions(Actions) :-
    maplist(is_stutter_action,Actions).

update_enabled_disabled_information_if_necessary(PGE,ActNameSuccessors,DisabledActionsAtCurState,EnabledActionsAtCurState) :-
    (is_pge_opt_on(PGE) ->
    compute_and_update_disabled_enabled_operations(ActNameSuccessors,DisabledActionsAtCurState,EnabledActionsAtCurState)
    ; true).