b_abstract_interpreter

absint_check_boolean_expression(b(Expr, _, _),LocalState,LocalStateOut,State,StateOut,Test) :-
    absint_check_boolean_expression2(Expr,LocalState,LocalStateOut,State,StateOut,Test).

absint_check_boolean_expression2(truth,LS,LS,S,S,true) :- !.

absint_check_boolean_expression2(falsity,LS,LS,S,S,false) :- !.

absint_check_boolean_expression2(conjunct(Arg1,Arg2),LocalStateIn,LocalStateIn,StateIn,StateOut,Test) :-
    !, absint_check_boolean_expression(Arg1,LocalStateIn,LocalStateIn,StateIn,TempStateOut,Result1),
    absint_check_boolean_expression(Arg2,LocalStateIn,LocalStateIn,TempStateOut,StateOut,Result2),
    (Result1 = Result2 -> Test = true ; Test = false).

absint_check_boolean_expression2(implication(Arg1,Arg2),LocalStateIn,LocalStateIn,StateIn,StateOut,Test) :-
    !, absint_check_boolean_expression(Arg1,LocalStateIn,LocalStateIn,StateIn,TempStateOut,Result1),
    absint_check_boolean_expression(Arg2,LocalStateIn,LocalStateIn,TempStateOut,StateOut,Result2),
    (Result1 = true, Result2 = false -> Test = false ; Test = true).

absint_check_boolean_expression2(BinExpr,LocalStateIn,LocalStateIn,StateIn,StateOut,Test) :-
    binary_operator(BinExpr, BOP, Arg1, Arg2), !,
    absint_compute_expression(Arg1,LocalStateIn,StateIn,Arg1Val),
    absint_compute_expression(Arg2,LocalStateIn,StateIn,Arg2Val),
    call_binary_test(BOP,Arg1Val,Arg2Val,NewVal1,NewVal2,Test),
    test_binary_update(Arg1, Arg2, NewVal1, NewVal2, StateIn, StateOut).

absint_check_boolean_expression2(Test,LocalState,_LocalStateOut,InState,_OutState,_) :-
    !, add_error_fail(absint_check_boolean_expression2, 'Boolean Expression not implemented: ', [Test,LocalState,InState]).

absint_compute_expression(b(Expr,Type,Info),LocalState,StateIn,Val) :-
    absint_compute_expression2(Expr,Type,Info,LocalState,StateIn,Val),!.

absint_compute_expression2(couple(Arg1,Arg2),_Type,_Info,LocalState,StateIn,couple(Arg1Val,Arg2Val)) :-
    !, absint_compute_expression(Arg1,LocalState,StateIn,Arg1Val),
    absint_compute_expression(Arg2,LocalState,StateIn,Arg2Val).

absint_compute_expression2(identifier(Key),_Type,_Info,LocalState,StateIn,Value) :-
    !, state_lookup(Key,LocalState,StateIn,Value).

absint_compute_expression2(integer(IntVal),Type,Info,_LocalState,_StateIn,AbsVal) :-
    !, call_alpha(integer(IntVal),Type,Info,AbsVal).

absint_compute_expression2(empty_set,Type,Info,_LocalState,_StateIn,AbsVal) :-
    !, call_alpha(empty_set,Type,Info,AbsVal).

absint_compute_expression2(boolean_true,Type,Info,_LocalState,_StateIn,AbsVal) :-
    !, call_alpha(boolean_true,Type,Info,AbsVal).

absint_compute_expression2(boolean_false,Type,Info,_LocalState,_StateIn,AbsVal) :-
    !, call_alpha(boolean_false,Type,Info,AbsVal).

absint_compute_expression2(Expr,_Type,_Info,LocalState,StateIn,AbsVal) :-
    unary_operator(Expr,OP,Arg), !,
    absint_compute_expression(Arg,LocalState,StateIn,ArgVal),
    call_unary_expression(OP,ArgVal,AbsVal).

absint_compute_expression2(Expr,_Type,_Info,LocalState,StateIn,AbsVal) :-
    binary_operator(Expr,OP,Arg1,Arg2), !,
    absint_compute_expression(Arg1,LocalState,StateIn,Arg1Val),
    absint_compute_expression(Arg2,LocalState,StateIn,Arg2Val),
    call_binary_expression(OP,Arg1Val,Arg2Val,AbsVal).

absint_compute_expression2(Expr,_Type,_Info,LocalState,StateIn,AbsVal) :-
    nary_operator(Expr,OP,Args), !,
    absint_compute_expressions(Args,LocalState,StateIn,ArgVals),
    call_nary_expression(OP,ArgVals,AbsVal).

absint_compute_expression2(X,T,I,LS,S,_V) :-
    !, add_error_fail(absint_compute_expression2, 'Expression not implemented: ', [X,T,I,LS,S]).

absint_compute_expressions([], _, _, []).

absint_compute_expressions([EXPRsHd|EXPRsTl],LocalState,InState,[ValHd|ValTl]) :-
    absint_compute_expression(EXPRsHd,LocalState,InState,ValHd),
    absint_compute_expressions(EXPRsTl,LocalState,InState,ValTl).

absint_execute_statement(b(Stmt,_,Infos),LocalState,InState,OutState,Path) :-
    absint_execute_statement2(Stmt,Infos,LocalState,InState,OutState,Path).

absint_execute_statement2(assign(VarExprs, ValExprs), _Infos,LocalState,InState,OutState,assign) :-
    !, absint_compute_expressions(ValExprs, LocalState, InState, ValExprs2),
    assign_vars(VarExprs, ValExprs2, LocalState, InState, NewVars, NewVals),
    assign_vals_to_vars(NewVars, NewVals, StoreList),
    OutState = StoreList.

absint_execute_statement2(assign_single_id(IDE,Expr),_Infos,LocalState,InState,OutState,assign) :-
    get_texpr_id(IDE,ID),!,
    absint_compute_expression(Expr,LocalState,InState,Value),
    OutState = [bind(ID,Value)].

absint_execute_statement2(if(IfList),_Infos,LocalState,InState,OutState,if) :-
    !, execute_else_list(IfList,LocalState,InState,OutState).

absint_execute_statement2(parallel(Statements),_Infos,LocalState,InState,OutState,parallel(Paths)) :-
    !, execute_statements_in_parallel(Statements, LocalState, InState, OutState, Paths).

absint_execute_statement2(select(Whens),_Infos,LocalState,InState,OutState,select(Nr,Path)) :-
    !, get_texpr_expr(TExpr,select_when(PreCond, Body)),
    nth1(Nr, Whens, TExpr),
    absint_check_boolean_expression(PreCond,LocalState,LocalStateOut,InState,NewInState,true),
    absint_execute_statement(Body,LocalStateOut,NewInState,OutState,Path).

absint_execute_statement2(Stmt,_Infos,LocalState,InState,_OutState,_Path) :-
    !, add_error_fail(absint_execute_statement2, 'Statement not implemented: ', [Stmt,LocalState,InState]).

absint_execute_top_level_statement(TExpr,LocalState,InState,OutState,Path) :-
    get_texpr_expr(TExpr,Stmt),
    absint_execute_top_level_statement2(Stmt,TExpr,LocalState,InState,OutState,Path).

absint_execute_top_level_statement2(precondition(PreCond,Body),_,LocalState,InState,OutState,Path) :-
    !, absint_check_boolean_expression(PreCond,LocalState,LocalStateOut,InState,TempState,true),
    absint_execute_statement(Body,LocalStateOut,TempState,OutState,Path).

absint_execute_top_level_statement2(_,TExpr,LocalState,InState,OutState,Path) :-
    absint_execute_statement(TExpr,LocalState,InState,OutState,Path).

execute_abstract_operation(Name,Operation,InState,NewOutState,ParaValues,ResultValues,TopLevel,Path) :-
    b_interpreter:b_get_machine_operation_for_animation(Name,Results,Parameters,Body,_OType,TopLevel),
    execute_abstract_operation(Name,Operation,InState,NewOutState,Body,Parameters,ParaValues,Results,ResultValues,TopLevel,Path).

execute_abstract_operation(Name,RealFullOperation,InState,SortedStateFinish,Body,Parameters,ParameterValues,Results,ResultValues,TopLevel,Path) :-
    absint_set_up_localstate(Parameters,ParameterValues,LocalState),
    absint_set_up_undefined_localstate(Results,InState,NewInState),
    (
    TopLevel==true
    -> absint_execute_top_level_statement(Body,LocalState,NewInState,Updates,Path)
    ; absint_execute_statement(Body,LocalState,NewInState,Updates,Path)
    ),
    l_expand_and_normalise_values(ParameterValues,NormalisedParaValues,Parameters),
    Operation =.. [Name|NormalisedParaValues],
    (
    Results == []
    -> RealFullOperation = Operation
    ; RealFullOperation = '-->'(Operation,ResultValues)
    ),
    state_store_list(Updates,NewInState,OutState),
    absint_get_results(Results,OutState,ResultValues,StateFinish),
    samsort(StateFinish,SortedStateFinish).

execute_abstract_top_level_operation(Name,FullOperation,InState,NewState,Parameters,Results,Path) :-
    b_interpreter:try_get_op_name(FullOperation, Name),
    execute_abstract_operation(Name,FullOperation,InState,NewState,Parameters,Results,true,Path).

find_abstract_transition(Operation, StateBegin, StateTrans, Paras, Results) :-
    execute_abstract_top_level_operation(Operation, _, StateBegin, StateTransInter, Paras, Results, Path),
    Path \= precond(false),
    StateTransInter = StateTrans.