units

all_operations([],State,State).

all_operations([Operation|T],InState,OutState) :-
    copy_term(InState,StoredInState),
    (do_transition(InState,OpSpec,IntermediateState,[op(Operation)])), !,
    (state_was_updated(StoredInState,IntermediateState)
    -> append_to_tcltk_replay_sequence(OpSpec)
    ; true),%format('Operation ~w did not update~nInState:~n~w~nIntermediateState:~n~w~n', [OpSpec,StoredInState,IntermediateState])),
    (halt_on_error
    -> OutState=IntermediateState
    ; all_operations(T,IntermediateState,OutState)).

all_operations([_Operation|T],InState,OutState) :-
    all_operations(T,InState,OutState),
    (halt_on_error
    -> OutState=InState
    ; all_operations(T,InState,OutState)),
    add_error(units_all_operations, 'operation could not be evaluated'),
    '$NOT_COVERED'('This should not happen').

another_iteration(StoredState,PossibleFixPointState) :-
    \+(halt_on_error), state_was_updated(StoredState,PossibleFixPointState).

do_check_invariant(ID,_CurState) :-
    %write(do_check_invariant(ID,CurState)), nl,
    invariant_violated(ID), !.

do_check_invariant(ID,CurState) :-
    set_units_error_context(checking_invariant),
    state_corresponds_to_initialised_b_machine(CurState,CurBState),
    execute_invariant(CurBState),
    set_invariant_checked(ID).

do_initialisation(OpSetup, concrete_constants(ConstantsState), [initialisation]) :-
    bmachine:bmachine_is_precompiled,
    b_machine_has_constants_or_properties, !,
    set_units_error_context(operation('SETUP_CONSTANTS',ConstantsState)),
    init_user_defined_alias,
    b_get_machine_constants(Constants),
    units_build_initial_state(Constants,ConstantsState),
    b_get_properties_from_machine(Properties),
    units_check_boolean_expression(Properties,ConstantsState,[]),
    ((get_preference(show_initialisation_arguments,true),extract_value_list(ConstantsState,Vals))
    -> safe_univ(OpSetup,['$setup_constants'|Vals])
    ; (OpSetup = '$setup_constants')
).

do_initialisation(Operation,StateOut,[initialisation]) :-
    bmachine:bmachine_is_precompiled,
    \+ b_machine_has_constants_or_properties, !,
    set_units_error_context(operation('$initialise_machine',StateOut)),
    init_user_defined_alias,
    b_get_machine_variables(Variables),
    units_build_initial_state(Variables,VariablesState),
    b_get_initialisation_from_machine(Init,_OType),
    units_execute_statement(Init,[],VariablesState,StateOut,_Path),
    specfile:create_initialisation_operation(StateOut,Operation).

do_transition(concrete_constants(StateIn),Operation,StateOut,[op(Operation)]) :-
    bmachine:bmachine_is_precompiled, !,
    set_units_error_context(operation('$initialise_machine',StateIn)),
    b_get_machine_variables(Variables),
    units_build_initial_state(Variables,VariablesState),
    append(StateIn,VariablesState,State),
    b_get_initialisation_from_machine(Init,_OType),
    units_execute_statement(Init,[],State,UnsortedStateOut,_Path),
    samsort(UnsortedStateOut,StateOut),
    specfile:create_initialisation_operation(StateOut,Operation).

do_transition(State,OpSpec,NewState,[op(Operation)]) :-
    bmachine:bmachine_is_precompiled,
    b_top_level_operation(Operation),
    set_units_error_context(operation(Operation,State)),
    units_find_transition(Operation, State, NewState, Paras, Results),
    (Paras \= []
    -> OpSpec1 =.. [Operation|Paras]
    ; OpSpec1 = Operation
    ),
    (Results \= []
    -> OpSpec = '-->'(OpSpec1,Results)
    ; OpSpec = OpSpec1
    ),
    execute_invariant(NewState).

execute_invariant(CurState) :-
    set_units_error_context(checking_invariant),
    b_get_properties_from_machine(Properties),
    units_check_boolean_expression(Properties,CurState,[]),
    b_get_invariant_from_machine(I),
    units_check_boolean_expression(I,[],CurState),
    set_units_error_context(checking_assertions),
    b_get_static_assertions_from_machine(StaticAssertions),
    units_check_list_of_boolean_expressions(StaticAssertions,[],CurState),
    b_get_dynamic_assertions_from_machine(DynamicAssertions),
    units_check_list_of_boolean_expressions(DynamicAssertions,[],CurState).

expand_variables([],[],_Result).

expand_variables([b(identifier(X),Type,Infos)|T],[b(identifier(X),Type,Infos2)|T2],Result) :-
    member(bind(X,Val),Result), !,
    (
    member(unit(ExplicitUnit),Infos) -> convert_to_atom(ExplicitUnit,Atom), ajoin(['"',Atom,'"'],Output),
    Infos2 = [output_pragma('unit',Output)|Infos] ;
    pp(classic,Val,PP) -> ajoin(['"',PP,'"'],AtomPP),
    Infos2 = [output_pragma('inferred_unit',AtomPP)|Infos] ;
    Infos2 = Infos
    ),
    expand_variables(T,T2,Result).

expand_variables([b(identifier(X),Type,Infos)|T],[b(identifier(X),Type,Infos)|T2],Result) :-
    format('Warning: identifier ~w not in result\n', [X]),
    expand_variables(T,T2,Result),
    '$NOT_COVERED'('This should not happen.').

extract_unbound_in_constraint([],[]).

extract_unbound_in_constraint([bind(Var,Val)|T], [Var|RT]) :-
    involved_in_constraint(Val),
    extract_unbound_in_constraint(T,RT).

extract_unbound_in_constraint([bind(_Var,_Val)|T], RT) :-
    extract_unbound_in_constraint(T,RT).

find_state_property(State,Property):-
    member(bind(Var,Val),State),
    Property = '='(Var,Val).

global_pragma_output([],[]) :- '$NOT_COVERED'('GUI code not used in automatic tests').

global_pragma_output([alias(AliasName,Definition)|T],Codes) :-
    global_pragma_output(T,CodesTemp),
    insert_spacer_and_join(Definition,DefinitionCodes),
    ajoin(['/*@ unit_alias ', AliasName, ' ', DefinitionCodes, ' */'], CodePragma),
    safe_atom_codes(CodePragma,CodePragmaCodes),
    append(CodePragmaCodes,CodesTemp,Codes),
    '$NOT_COVERED'('GUI code not used in automatic tests').

halt_on_error :-
    preference(plugin(units,fixpoint_halt_on_error),true),
    state_error_exists.

insert_result_in_machine :-
    write('Pre-Check finished. Inserting results in machine'), nl,
    static_result(Result,_),
    full_b_machine(BMachine),
    get_section(abstract_variables,BMachine,AbsVarsContent),
    expand_variables(AbsVarsContent,ExpandedAbsVarsContent,Result),
    write_section(abstract_variables,ExpandedAbsVarsContent,BMachine,BMachine2),
    get_section(concrete_variables,BMachine2,ConcVarsContent),
    expand_variables(ConcVarsContent,ExpandedConcVarsContent,Result),
    write_section(concrete_variables,ExpandedConcVarsContent,BMachine2,BMachine3),
    get_section(abstract_constants,BMachine3,AbsConstContent),
    expand_variables(AbsConstContent,ExpandedAbsConstContent,Result),
    write_section(abstract_constants,ExpandedAbsConstContent,BMachine3,BMachine4),
    get_section(concrete_constants,BMachine4,ConcConstContent),
    expand_variables(ConcConstContent,ExpandedConcConstContent,Result),
    write_section(concrete_constants,ExpandedConcConstContent,BMachine4,BMachine5),
    retractall(bmachine:machine(_,_)),
    bmachine:assert_main_machine(BMachine5).

internal_representation(Rep) :-
    full_b_machine(BMachine),
    (static_result(_,_) -> true ; static_pre_check),
    translate:translate_machine1(BMachine,(0,RepWithoutGlobals),(_,[])),
    findall(alias(AliasName,Definition),
    global_pragma(unit_alias,[AliasName|Definition]),
    List),
    global_pragma_output(List,OutputCodes),
    append(OutputCodes,RepWithoutGlobals,Rep),
    '$NOT_COVERED'('GUI code not used in automatic tests').

notify_new_transition(FromID,TransID,DestID,_Exists) :-
    %write(notify_new_transition(FromID,TransID,DestID,Exists)),nl,
    state_space:transition(FromID,Action,TransID,DestID),
    set_units_error_context(operation(Action,_)),
    visited_expression(DestID,State),
    check_state_add_error(DestID,State).

output('Static Analysis Result', X, [tcltk,cli]) :-
    (static_result(FixPointState,UnboundInConstraint)
    -> pp_fixpoint_result(FixPointState,UnboundInConstraint,Output),
    atom_codes(Output,X)
    ; X = "no result yet"),
    '$NOT_COVERED'('GUI code not used in automatic tests').

output('Grounded Result State', X, [eclipse]) :-
    findall(Error,get_error(incorrect_unit_definition,Error),ListOfErrors),
    ListOfErrors \= [], !,
    % we have something to report. skip the rest
    reset_errors,
    X = error(ListOfErrors).

output('Grounded Result State', state(X), [eclipse]) :-
    (static_result(FixPointState,_UnboundInConstraint)
    -> maplist(pp(eventb),FixPointState,X)
    ; X = []).

plugin_info([
    % The name of the Plugin
    name = 'Unit Analysis'
    % Author is not used yet
    ,author = 'Sebastian Krings'
    % marks the plugin as unstable or stable
    ,status = stable
    % A list of supported file extensions together with a file description
    % (They are not used here because the plugin is used for an already loaded
    % file, see plugin_for_modes)
    % ,file_extensions = [ ('Plugin demonstration spec', ['.xtl2', '.PPP']) ]
    % The predicate that is used to load a file. The first argument is the
    % filename, the second the file extension (like '.mch').
    %,load_file = load_spec/1
    % The transition skeleton initialises a transition variable in such
    % way that only a part of all transitions match it. It is used to
    % separate time outs and maximum number of computations for several
    % transition classes (like different operations).
    %,transition_skeleton = trans_skel/1
    % The predicate that computes a transition in the state-space, its
    % arguments are SourceState,Operation,DestinationState,ListOfOperationInfos.
    ,transition = do_transition/4
    % The predicate that computes an initial state, its arguments are
    % Operation,DestinationState,ListOfOperationInfos.
    ,initialisation = do_initialisation/3
    % A predicate that returns a property for a given state, its arguments
    % are State,Property.
    ,state_property = find_state_property/2
    % A predicate that receives a list of expressions,predicates and
    % predicates on transitions as input (list of codes) and returns
    % the parsed expressions.
    % Its arguments are ListOfExpressionStrings,ListOfPredicateStrings,
    % ListOfTransitionPredicateStrings,ListOfExpressions,ListOfPredicates,
    % ListOfTransitionPredicates.
    %,parser = parse_spec/6
    % A predicate that computes a value of an expression (returned by
    % the parser above) in a state. Its arguments are Expression,State
    %,compute_expression = compute/2
    % A predicate that evaluates a predicate (returned by the parser above)
    % in a state. Its arguments are Predicate,State
    %,evaluate_predicate = eval/2
    % A predicate that evaluates a predicate (returned by the parser above)
    % for a transition. Its arguments are Predicate,Transition
    %,evaluate_transition = evaltrans/2
    % A predicate that checks if a state is initialised. Its argument is a State
    %,is_initialised_state = is_init/1
    % Pretty-print a transition, the first argument is the transition, the
    % second -the result- is a list of codes.
    ,prettyprint_transition = pp_trans/2
    % Pretty-print a property, the first argument is the property, the
    % second -the result- is a list of codes.
    ,prettyprint_property = pp_prop/2
    ,prettyprint_value = pp_value/2
    % Syntax colouring is defined by specifying a list of rules, each
    % containing of a regular expression and a colour class
    %,syntax_colouring = [pair('/\\*', '\\*/',syntax_comment),
    % expression('(?=\\m)(start|trans|prop)(?=\\M)', syntax_keyword),
    % expression('(?=\\m)(true|fail|atomic|nonvar|var|functor|op|is|ground|member|append|length)(?=\\M)|=', syntax_type),
    % expression(':-|!|-->|;|\\.', syntax_assignment),
    % expression('%(.*)', syntax_comment)]
    ,plugin_for_modes = [b]
    ,plugin_init=plugin_init/0
    ,new_transition_notification=notify_new_transition/4
    ,check_invariant=do_check_invariant/2
    ,preferences=preference/4
    ,output=output/3
    ,internal_representation=internal_representation/1
    ]).

plugin_init :-
    units_interpreter_helpers:retractall(cached_global_type(_,_)),
    retractall(tcltk_replay_sequence(_)),
    reset_tcltk_replay_sequence,
    state_space:state_space_initialise,
    (preference(plugin(units,fixpoint_on_load),true)
    -> static_pre_check
    ; true),
    (replay_tcltk_sequence ; write('Could not replay Tcl/Tk Operation Sequence!'), nl).

pp_prop(Property,Pretty) :-
    units_pp_prop(Property,Pretty).

pp_trans(Transition,Pretty) :-
    units_pp_trans(Transition,Pretty).

pp_value(Value,Pretty) :-
    units_pp_value(Value,Pretty).

preference(fixpoint_on_load, true, 'Perform Static Fix-Point Check on Startup',bool).

preference(fixpoint_halt_on_error, true, 'Halt Fix-Point Search on Error',bool).

preference(fixpoint_max_iterations, 100, 'Max. Number of Iterations in Fix-Point Check', nat1).

set_units_error_context(Context) :-
    retractall(units_error_context(_)),
    assertz(units_error_context(Context)).

static_pre_check :-
    % pre check can only be performed on an initialised machine
    bmachine:bmachine_is_precompiled,
    statistics(walltime,[Start|_]),
    retractall(iterations(_)),
    assertz(iterations(0)),
    do_initialisation(Operation, State, [initialisation]),
    append_to_tcltk_replay_sequence(Operation),
    to_fixpoint(State,FixPointState),
    retractall(static_result(_,_)),
    extract_unbound_in_constraint(FixPointState,Unbound),
    assertz(static_result(FixPointState,Unbound)),
    insert_result_in_machine,
    iterations(It),
    statistics(walltime, [End|_]),
    Time is End - Start,
    format('Fixpoint algorithm stopped after ~w iterations and ~w milliseconds ~n', [It, Time]).

static_pre_check :- write('Pre-Check failed!\n'), '$NOT_COVERED'('This should not happen').

to_fixpoint(State,FixPointState) :-
    retract(iterations(LastIt)), preference(plugin(units,fixpoint_max_iterations),MaxIt),
    LastIt < MaxIt
    -> CurIt is LastIt + 1, assertz(iterations(CurIt)), to_fixpoint2(State,FixPointState)
    ; State=FixPointState, add_warning(units, 'Warning: Fixpoint algorithm stopped, because iteration limit was reached\n').

to_fixpoint2(concrete_constants(State),FixPointState) :-
    !, do_transition(concrete_constants(State),Op,PossibleFixPointState,_Op2),
    append_to_tcltk_replay_sequence(Op),
    to_fixpoint(PossibleFixPointState,FixPointState).

to_fixpoint2(State,FixPointState) :-
    findall(Operation, do_transition(State,_,_,[op(Operation)]), ListOfOperations),
    copy_term(State,StoredState),
    all_operations(ListOfOperations,State,PossibleFixPointState),
    (
    another_iteration(StoredState,PossibleFixPointState)
    -> to_fixpoint(PossibleFixPointState,FixPointState)
    ; FixPointState = PossibleFixPointState
).