alloy2b

add_constraint_for_seq_field('is_seq'(_,_,_), TSignatureName, TempPred, TFieldID, TPred) :-
    !,
    % !_s.(_s : TSignatureName => dom(TFieldID)[{_s}] = 0..card(dom(TFieldID)[{_s}])-1)
    TPred = conjunct(BPOS,TempPred,forall([identifier(BPOS,'_s')],
    implication(BPOS,member(identifier(BPOS,'_s'),TSignatureName),
    equal(BPOS,image(BPOS,domain(BPOS,TFieldID),set_extension(BPOS,[identifier(BPOS,'_s')])),
    interval(BPOS,integer(BPOS,0),minus(BPOS,card(BPOS,image(BPOS,domain(BPOS,TFieldID),
    set_extension(BPOS,[identifier(BPOS,'_s')]))),integer(BPOS,1))))))).

add_constraint_for_seq_field(_, _, Pred, _, Pred).

add_constraint_for_someof_field(someof(_,_,_), TempPred, TSignatureName, TPred) :-
    !,
    TempPred = member(BPOS,TFieldID,_),
    TPred = conjunct(BPOS,equal(BPOS,domain(BPOS,TFieldID),TSignatureName),TempPred).

add_constraint_for_someof_field(_, Pred, _, Pred).

add_error_for_univ_or_iden(Src, Op, Arg1, Arg2) :-
    binary_op_not_allowing_iden_or_univ(Op),
    ( ground(Arg1),
    is_iden(Arg1)
    ; ground(Arg2),
    is_iden(Arg2)
    ),
    atom_concat('iden keyword in Alloy operator ', Op, Msg),
    add_error_not_supported(Src, Msg).

add_error_for_univ_or_iden(Src, Op, Arg1, Arg2) :-
    binary_op_not_allowing_iden_or_univ(Op),
    ( ground(Arg1),
    is_univ(Arg1)
    ; ground(Arg2),
    is_univ(Arg2)
    ),
    atom_concat('univ keyword in Alloy operator ', Op, Msg),
    add_error_not_supported(Src, Msg).

add_error_not_supported(Src, NotSupported) :-
    atom(NotSupported),
    add_error(Src, 'Expression not supported by our translation: ', [NotSupported]).

alloy_constant_to_b(none, BPOS, empty_set(BPOS)).

alloy_constant_to_b('boolean''False', BPOS, boolean_false(BPOS)).

alloy_constant_to_b('boolean''True', BPOS, boolean_true(BPOS)).

alloy_constant_to_b('boolean''Bool', BPOS, bool_set(BPOS)).

alloy_expr_contains_join(AndOr) :-
    AndOr =.. [Functor,ListOfAsts,_Pos],
    !,
    member(Functor, [and,or]),
    member(Ast, ListOfAsts),
    alloy_expr_contains_join(Ast),
    !.

alloy_expr_contains_join(join(_,_,_Type,_Pos)).

alloy_expr_contains_join(Expr) :-
    Expr =.. [_Functor,Arg1,Arg2,_Type,_Pos],
    !,
    ( alloy_expr_contains_join(Arg1) ->
    true
    ; alloy_expr_contains_join(Arg2)
).

alloy_expr_contains_join(Expr) :-
    Expr =.. [_Functor,Arg,_Type,_Pos],
    alloy_expr_contains_join(Arg).

alloy_expr_contains_join(Expr) :-
    Expr =.. [Functor,_Params,Fields,Body,_Type,_POS],
    member(Functor, [all,no,some,one,lone,comprehension]),
    ( alloy_expr_contains_join(Body) ->
    true
    ; member(F, Fields),
    alloy_expr_contains_join(F) ->
    true
).

alloy_natural_id(Id, Suffix) :-
    atom(Id),
    module_in_scope_but_root('util''natural', Alias),
    atom_concat(Alias, '\'', Prefix),
    atom_concat(Prefix, Suffix, Id).

alloy_to_b_binary_operator(in, subset).

alloy_to_b_binary_operator(not_in, not_subset).

alloy_to_b_binary_operator(plus, union).

alloy_to_b_binary_operator(or, disjunct). % actually treated as unary operator

alloy_to_b_binary_operator(and, conjunct). % actually treated as unary operator

alloy_to_b_binary_operator(minus, set_subtraction).

alloy_to_b_binary_operator(function, expression_definition).

alloy_to_b_binary_operator(predicate, predicate_definition).

alloy_to_b_binary_operator(not_equal, not_equal).

alloy_to_b_binary_operator(dom_restr, domain_restriction). % not ok for ternary, set must be unary

alloy_to_b_binary_operator(ran_restr, range_restriction). % also ok for ternary, ... relations

alloy_to_b_binary_operator(equal, equal).

alloy_to_b_binary_operator(conjunct, conjunct).

alloy_to_b_binary_operator(intersection, intersection).

alloy_to_b_binary_operator(implication, implication).

alloy_to_b_binary_operator(iff, equivalence).

alloy_to_b_binary_operator(override, overwrite). % ++

alloy_to_b_boolean_utility_function('boolean''Not', [TP1], BPOS, Result) :-
    !,
    Result = convert_bool(BPOS,equal(BPOS,TP1,boolean_false(BPOS))).

alloy_to_b_boolean_utility_function('boolean''isTrue', [TP1], BPOS, Result) :-
    !,
    Result = equal(BPOS,TP1,boolean_true(BPOS)).

alloy_to_b_boolean_utility_function('boolean''isFalse', [TP1], BPOS, Result) :-
    !,
    Result = equal(BPOS,TP1,boolean_false(BPOS)).

alloy_to_b_boolean_utility_function('boolean''And', [TP1,TP2], BPOS, Result) :-
    !,
    Result = convert_bool(BPOS,conjunct(BPOS,equal(BPOS,TP1,boolean_true(BPOS)),equal(BPOS,TP2,boolean_true(BPOS)))).

alloy_to_b_boolean_utility_function('boolean''Or', [TP1,TP2], BPOS, Result) :-
    !,
    Result = convert_bool(BPOS,disjunct(BPOS,equal(BPOS,TP1,boolean_true(BPOS)),equal(BPOS,TP2,boolean_true(BPOS)))).

alloy_to_b_boolean_utility_function('boolean''Nand', [TP1,TP2], BPOS, Result) :-
    !,
    Result = convert_bool(BPOS,disjunct(BPOS,equal(BPOS,TP1,boolean_false(BPOS)),equal(BPOS,TP2,boolean_false(BPOS)))).

alloy_to_b_boolean_utility_function('boolean''Nor', [TP1,TP2], BPOS, Result) :-
    !,
    Result = convert_bool(BPOS,conjunct(BPOS,equal(BPOS,TP1,boolean_false(BPOS)),equal(BPOS,TP2,boolean_false(BPOS)))).

alloy_to_b_boolean_utility_function('boolean''Xor', [TP1,TP2], BPOS, Result) :-
    !,
    LHS = conjunct(BPOS,equal(BPOS,TP1,boolean_false(BPOS)),equal(BPOS,TP2,boolean_true(BPOS))),
    RHS = conjunct(BPOS,equal(BPOS,TP1,boolean_true(BPOS)),equal(BPOS,TP2,boolean_false(BPOS))),
    Result = convert_bool(BPOS,disjunct(BPOS,LHS,RHS)).

alloy_to_b_boolean_utility_function(FunName, _, BPOS, truth(BPOS)) :-
    atom_prefix('boolean', FunName),
    !,
    add_error(alloy_to_b_boolean_utility_function, 'Function from util/boolean currently not supported', [], BPOS).

alloy_to_b_integer_func('''min', 1, min, set, integer).

alloy_to_b_integer_func('''max', 1, max, set, integer).

alloy_to_b_integer_func('''min', 0, min_int, set, integer). % TO DO: investigate bit-width related translation

alloy_to_b_integer_func('''max', 0, max_int, set, integer).

alloy_to_b_integer_natural_utility_func(FunName, Arity, BOp, ArgType, ReturnType) :-
    is_util_integer_natural_func(FunName, _, AlloyOp),
    ( alloy_to_b_integer_func(AlloyOp, Arity, BOp, ArgType, ReturnType)
    ; alloy_to_b_integer_operator_func(AlloyOp, Arity, BOp, ArgType, ReturnType)
    ; alloy_to_b_integer_to_integer_func(AlloyOp, Arity, BOp, ArgType, ReturnType)
    ; alloy_to_b_operator_func(AlloyOp, Arity, BOp, ArgType, ReturnType)
    ),!.

alloy_to_b_integer_operator(less, less).

alloy_to_b_integer_operator(greater, greater).

alloy_to_b_integer_operator(less_equal, less_equal).

alloy_to_b_integer_operator(greater_equal, greater_equal).

alloy_to_b_integer_operator_func('''gt', 2, greater, integer, set).

alloy_to_b_integer_operator_func('''lt', 2, less, integer, set).

alloy_to_b_integer_operator_func('''gte', 2, greater_equal, integer, set).

alloy_to_b_integer_operator_func('''lte', 2, less_equal, integer, set).

alloy_to_b_integer_operator_func('''eq', 2, equal, integer, set).

alloy_to_b_integer_to_integer_func('''minus', 2, minus, integer, integer).

alloy_to_b_integer_to_integer_func('''plus', 2, add, integer, integer).

alloy_to_b_integer_to_integer_func('''div', 2, div, integer, integer).

alloy_to_b_integer_to_integer_func('''mul', 2, multiplication, integer, integer).

alloy_to_b_integer_to_integer_func('''rem', 2, modulo, integer, integer).

alloy_to_b_integer_to_integer_func('''add', 2, add, integer, integer).

alloy_to_b_integer_to_integer_func('''sub', 2, minus, integer, integer).

alloy_to_b_integer_to_integer_func('''negate', 1, unary_minus, integer, integer).

alloy_to_b_integer_to_integer_func('''next', 1, successor, integer, integer). % not sure this is called; seems to call arity 0 and use join

alloy_to_b_integer_to_integer_func('''prev', 1, predecessor, integer, integer).

alloy_to_b_integer_utility_function('''signum', BPOS, [P1Int], Result) :-
    !,
    % IF int(p) < 0 THEN -1 ELSE IF int(p) > 0 THEN 1 ELSE 0 END END
    Result = if_then_else(BPOS,less(BPOS,P1Int,integer(BPOS,0)),set_extension(BPOS,[integer(BPOS,-1)]),if_then_else(BPOS,greater(BPOS,P1Int,integer(BPOS,0)),set_extension(BPOS,[integer(BPOS,1)]),set_extension(BPOS,[integer(BPOS,0)]))).

alloy_to_b_integer_utility_function('''zero', BPOS, [P1Int], Result) :-
    !,
    % int(p) = 0
    Result = equal(BPOS,P1Int,integer(BPOS,0)).

alloy_to_b_integer_utility_function(Name, BPOS, [P1Int], Result) :-
    ( Name == '''pos', BOp = greater
    ; Name == '''neg', BOp = less),
    !,
    translate_e_p_integer(P1Int, P1Int),
    % int(p) > 0 or int(p) < 0
    Result =.. [BOp,BPOS,P1Int,integer(BPOS,0)].

alloy_to_b_integer_utility_function(Name, BPOS, [P1Int], Result) :-
    ( Name == '''nonpos', BOp = less_equal
    ; Name == '''nonneg', BOp = greater_equal),
    !,
    translate_e_p_integer(P1Int, P1Int),
    % int(p) <= 0 or int(p) >= 0
    Result =.. [BOp,BPOS,P1Int,integer(BPOS,0)].

alloy_to_b_integer_utility_function(Name, BPOS, [P1Int,P2Int], Result) :-
    ( Name == '''smaller', BOp = min
    ; Name == '''larger', BOp = max),
    !,
    % {min({int(p1),int(p2)})} or {max({int(p1),int(p2)})}
    Inner =.. [BOp,BPOS,set_extension(BPOS,[P1Int,P2Int])],
    Result = set_extension(BPOS,[Inner]).

alloy_to_b_integer_utility_function(Name, BPOS, [P1Int], Result) :-
    ( Name == '''nexts', BOp = greater
    ; Name == '''prevs', BOp = less),
    !,
    % {x | x : INTEGER & x > int(p)} or {x | x : INTEGER & x < int(p)}
    Inner =.. [BOp,BPOS,identifier(BPOS,x),P1Int],
    integer_type(IntOrInteger),
    check_position(BPOS,alloy_to_b_integer_utility_function(Name)),
    Result = comprehension_set(BPOS,[identifier(BPOS,x)],
    conjunct(BPOS,member(BPOS,identifier(BPOS,x),integer_set(none,IntOrInteger)),Inner)).

alloy_to_b_natural_utility_function('''ord''first', BPOS, [], set_extension(BPOS,[integer(BPOS,0)])).

alloy_to_b_natural_utility_function('''ord''last', BPOS, [], set_extension(BPOS,[max_int(BPOS)])).

alloy_to_b_natural_utility_function('''ord''next', BPOS, [P1Int], set_extension(BPOS,[add(BPOS,P1Int,integer(BPOS,1))])).

alloy_to_b_natural_utility_function('''ord''prev', BPOS, [P1Int], set_extension(BPOS,[minus(BPOS,P1Int,integer(BPOS,1))])).

alloy_to_b_natural_utility_function('''One', BPOS, [], set_extension(BPOS,[integer(BPOS,1)])).

alloy_to_b_natural_utility_function('''Zero', BPOS, [], set_extension(BPOS,[integer(BPOS,0)])).

alloy_to_b_natural_utility_function('''min', BPOS, [], set_extension(BPOS,[max(BPOS,set_extension(BPOS,[integer(BPOS,0),min_int(BPOS)]))])).

alloy_to_b_natural_utility_function('''inc', BPOS, [P1Int], set_extension(BPOS,[add(BPOS,P1Int,integer(BPOS,1))])).

alloy_to_b_natural_utility_function('''dec', BPOS, [P1Int], set_extension(BPOS,[minus(BPOS,P1Int,integer(BPOS,1))])).

alloy_to_b_operator(Op, BOp) :-
    alloy_to_b_unary_operator(Op, BOp),
    !.

alloy_to_b_operator(Op, BOp) :-
    alloy_to_b_binary_operator(Op, BOp),
    !.

alloy_to_b_operator(Op, Op) :-
    format('~n~nTRANSLATING ~w to B without modification!~n', [Op]).

alloy_to_b_operator_func('''next', 0, successor, set, set).

alloy_to_b_operator_func('''prev', 0, predecessor, set, set).

alloy_to_b_relational_utility_function(UtilFunName, [TRelation], BPOS, TCall) :-
    module_in_scope_but_root('util\'relation', RelationAlias),
    atom_concat(RelationAlias, '\'dom', UtilFunName),
    !,
    TCall = domain(BPOS,TRelation).

alloy_to_b_relational_utility_function(UtilFunName, [TRelation], BPOS, TCall) :-
    module_in_scope_but_root('util\'relation', RelationAlias),
    atom_concat(RelationAlias, '\'ran', UtilFunName),
    !,
    TCall = range(BPOS,TRelation).

alloy_to_b_relational_utility_function(UtilFunName, [TRelation,TDomain], BPOS, TCall) :-
    module_in_scope_but_root('util\'relation', RelationAlias),
    atom_concat(RelationAlias, '\'total', UtilFunName),
    !,
    ID0 = identifier(BPOS,x),
    LHS = member(BPOS,ID0,TDomain),
    RHS = not_equal(BPOS,image(BPOS,TRelation,set_extension(BPOS,[ID0])),empty_set(BPOS)),
    TCall = forall(BPOS,[ID0],implication(BPOS,LHS,RHS)).

alloy_to_b_relational_utility_function(UtilFunName, [TRelation,TDomain], BPOS, TCall) :-
    module_in_scope_but_root('util\'relation', RelationAlias),
    atom_concat(RelationAlias, '\'functional', UtilFunName),
    !,
    ID0 = identifier(BPOS,x),
    LHS = member(BPOS,ID0,TDomain),
    RHS = less_equal(BPOS,card(BPOS,image(BPOS,TRelation,set_extension(BPOS,[ID0]))),integer(BPOS,1)),
    TCall = forall(BPOS,[ID0],implication(BPOS,LHS,RHS)).

alloy_to_b_relational_utility_function(UtilFunName, [TRelation,TDomain], BPOS, TCall) :-
    module_in_scope_but_root('util\'relation', RelationAlias),
    atom_concat(RelationAlias, '\'function', UtilFunName),
    !,
    ID0 = identifier(BPOS,x),
    LHS = member(BPOS,ID0,TDomain),
    RHS = equal(BPOS,card(BPOS,image(BPOS,TRelation,set_extension(BPOS,[ID0]))),integer(BPOS,1)),
    TCall = forall(BPOS,[ID0],implication(BPOS,LHS,RHS)).

alloy_to_b_relational_utility_function(UtilFunName, [TRelation,TCodomain], BPOS, TCall) :-
    module_in_scope_but_root('util\'relation', RelationAlias),
    atom_concat(RelationAlias, '\'injective', UtilFunName),
    !,
    ID0 = identifier(BPOS,y),
    LHS = member(BPOS,ID0,TCodomain),
    RHS = less_equal(BPOS,card(BPOS,image(BPOS,reverse(BPOS,TRelation),set_extension(BPOS,[ID0]))),integer(BPOS,1)),
    TCall = forall(BPOS,[ID0],implication(BPOS,LHS,RHS)).

alloy_to_b_relational_utility_function(UtilFunName, [TRelation,TCodomain], BPOS, TCall) :-
    module_in_scope_but_root('util\'relation', RelationAlias),
    atom_concat(RelationAlias, '\'surjective', UtilFunName),
    !,
    ID0 = identifier(BPOS,y),
    LHS = member(BPOS,ID0,TCodomain),
    RHS = not_equal(BPOS,image(BPOS,reverse(BPOS,TRelation),set_extension(BPOS,[ID0])),empty_set(BPOS)),
    TCall = forall(BPOS,[ID0],implication(BPOS,LHS,RHS)).

alloy_to_b_relational_utility_function(UtilFunName, [TRelation,TCodomain], BPOS, TCall) :-
    module_in_scope_but_root('util\'relation', RelationAlias),
    atom_concat(RelationAlias, '\'bijective', UtilFunName),
    !,
    ID0 = identifier(BPOS,y),
    LHS = member(BPOS,ID0,TCodomain),
    RHS = equal(BPOS,card(BPOS,image(BPOS,reverse(BPOS,TRelation),set_extension(BPOS,[ID0]))),integer(BPOS,1)),
    TCall = forall(BPOS,[ID0],implication(BPOS,LHS,RHS)).

alloy_to_b_relational_utility_function(UtilFunName, [Relation,Domain,Codomain], BPOS, TCall) :-
    module_in_scope_but_root('util\'relation', RelationAlias),
    atom_concat(RelationAlias, '\'bijection', UtilFunName),
    !,
    atom_concat(RelationAlias, '\'function', Function),
    atom_concat(RelationAlias, '\'bijective', Bijective),
    alloy_to_b_relational_utility_function(Function, [Relation,Domain], BPOS, IsFunction),
    alloy_to_b_relational_utility_function(Bijective, [Relation,Codomain], BPOS, IsBijective),
    TCall = conjunct(BPOS,IsFunction,IsBijective).

alloy_to_b_relational_utility_function(UtilFunName, [TRelation1,TRelation2], BPOS, TCall) :-
    module_in_scope_but_root('util\'relation', RelationAlias),
    atom_concat(RelationAlias, '\'reflexive', UtilFunName),
    !,
    TCall = subset(BPOS,identity(BPOS,TRelation2),TRelation1).

alloy_to_b_relational_utility_function(UtilFunName, [TRelation], BPOS, TCall) :-
    module_in_scope_but_root('util\'relation', RelationAlias),
    atom_concat(RelationAlias, '\'irreflexive', UtilFunName),
    !,
    TCall = equal(BPOS,intersection(BPOS,identity(BPOS,domain(BPOS,TRelation)),TRelation),empty_set(BPOS)).

alloy_to_b_relational_utility_function(UtilFunName, [TRelation], BPOS, TCall) :-
    module_in_scope_but_root('util\'relation', RelationAlias),
    atom_concat(RelationAlias, '\'symmetric', UtilFunName),
    !,
    TCall = subset(BPOS,reverse(BPOS,TRelation),TRelation).

alloy_to_b_relational_utility_function(UtilFunName, [TRelation], BPOS, TCall) :-
    module_in_scope_but_root('util\'relation', RelationAlias),
    atom_concat(RelationAlias, '\'antisymmetric', UtilFunName),
    !,
    Intersection = intersection(BPOS,reverse(BPOS,TRelation),TRelation),
    TCall = subset(BPOS,Intersection,identity(BPOS,domain(BPOS,TRelation))).

alloy_to_b_relational_utility_function(UtilFunName, [TRelation], BPOS, TCall) :-
    module_in_scope_but_root('util\'relation', RelationAlias),
    atom_concat(RelationAlias, '\'transitive', UtilFunName),
    !,
    TCall = subset(BPOS,composition(BPOS,TRelation,TRelation),TRelation).

alloy_to_b_relational_utility_function(UtilFunName, [TRelation1,TRelation2], BPOS, TCall) :-
    module_in_scope_but_root('util\'relation', RelationAlias),
    atom_concat(RelationAlias, '\'acyclic', UtilFunName),
    !,
    ID0 = identifier(BPOS,x),
    TCall = forall(BPOS,[ID0],implication(BPOS,member(BPOS,ID0,TRelation2),
    not_member(BPOS,couple(BPOS,ID0,ID0),closure(BPOS,TRelation1)))).

alloy_to_b_relational_utility_function(UtilFunName, [TRelation1,TRelation2], BPOS, TCall) :-
    module_in_scope_but_root('util\'relation', RelationAlias),
    atom_concat(RelationAlias, '\'complete', UtilFunName),
    !,
    ID0 = identifier(BPOS,x),
    ID1 = identifier(BPOS,y),
    LHS = conjunct(BPOS,conjunct(BPOS,member(BPOS,ID0,TRelation2),member(BPOS,ID1,TRelation2)),not_equal(BPOS,ID0,ID1)),
    RHS = member(BPOS,couple(BPOS,ID0,ID1),union(BPOS,TRelation1,reverse(BPOS,TRelation1))),
    TCall = forall(BPOS,[ID0,ID1],implication(BPOS,LHS,RHS)).

alloy_to_b_relational_utility_function(UtilFunName, [Relation1,Relation2], BPOS, TCall) :-
    module_in_scope_but_root('util\'relation', RelationAlias),
    atom_concat(RelationAlias, '\'preorder', UtilFunName),
    !,
    atom_concat(RelationAlias, '\'reflexive', Reflexive),
    atom_concat(RelationAlias, '\'transitive', Transitive),
    alloy_to_b_relational_utility_function(Reflexive, [Relation1,Relation2], BPOS, IsReflexive),
    alloy_to_b_relational_utility_function(Transitive, [Relation1], BPOS, IsTransitive),
    TCall = conjunct(BPOS,IsReflexive,IsTransitive).

alloy_to_b_relational_utility_function(UtilFunName, [Relation1,Relation2], BPOS, TCall) :-
    module_in_scope_but_root('util\'relation', RelationAlias),
    atom_concat(RelationAlias, '\'equivalence', UtilFunName),
    !,
    atom_concat(RelationAlias, '\'preorder', Preorder),
    atom_concat(RelationAlias, '\'symmetric', Symmetric),
    alloy_to_b_relational_utility_function(Preorder, [Relation1,Relation2], BPOS, IsReflexive),
    alloy_to_b_relational_utility_function(Symmetric, [Relation1], BPOS, IsTransitive),
    TCall = conjunct(BPOS,IsReflexive,IsTransitive).

alloy_to_b_relational_utility_function(UtilFunName, [Relation1,Relation2], BPOS, TCall) :-
    module_in_scope_but_root('util\'relation', RelationAlias),
    atom_concat(RelationAlias, '\'partialOrder', UtilFunName),
    !,
    atom_concat(RelationAlias, '\'preorder', Preorder),
    atom_concat(RelationAlias, '\'antisymmetric', Antisymmetric),
    alloy_to_b_relational_utility_function(Preorder, [Relation1,Relation2], BPOS, IsReflexive),
    alloy_to_b_relational_utility_function(Antisymmetric, [Relation1], BPOS, IsTransitive),
    TCall = conjunct(BPOS,IsReflexive,IsTransitive).

alloy_to_b_relational_utility_function(UtilFunName, [Relation1,Relation2], BPOS, TCall) :-
    module_in_scope_but_root('util\'relation', RelationAlias),
    atom_concat(RelationAlias, '\'totalOrder', UtilFunName),
    !,
    atom_concat(RelationAlias, '\'partialOrder', Partialorder),
    atom_concat(RelationAlias, '\'complete', Complete),
    alloy_to_b_relational_utility_function(Partialorder, [Relation1,Relation2], BPOS, IsReflexive),
    alloy_to_b_relational_utility_function(Complete, [Relation1,Relation2], BPOS, IsTransitive),
    TCall = conjunct(BPOS,IsReflexive,IsTransitive).

alloy_to_b_relational_utility_function(FunName, _, BPOS, truth(BPOS)) :-
    module_in_scope_but_root('util\'relation', RelationAlias),
    atom_prefix(RelationAlias, FunName),
    !,
    add_error(alloy_to_b_relational_utility_function, 'Function from util/relation currently not supported', [], BPOS).

alloy_to_b_special_multiplicity_type(total_relation, BPOS, TRel, TMDom, TMRan, relations(BPOS,TMDom,TMRan), AdditionalConstraint, no) :-
    AdditionalConstraint = equal(BPOS,domain(BPOS,TRel),TMDom).

alloy_to_b_special_multiplicity_type(total_function, BPOS, _, TMDom, TMRan, total_function(BPOS,TMDom,TMRan), none, no).

alloy_to_b_special_multiplicity_type(partial_function, BPOS, _, TMDom, TMRan, partial_function(BPOS,TMDom,TMRan), none, no).

alloy_to_b_special_multiplicity_type(surjection_relation, BPOS, TRel, TMDom, TMRan, relations(BPOS,TMDom,TMRan), AdditionalConstraint, no) :-
    AdditionalConstraint = equal(BPOS,range(BPOS,TRel),TMRan).

alloy_to_b_special_multiplicity_type(total_surjection_relation, BPOS, TRel, TMDom, TMRan, relations(BPOS,TMDom,TMRan), AdditionalConstraint, no) :-
    AdditionalConstraint = conjunct(BPOS,equal(BPOS,domain(BPOS,TRel),TMDom),equal(BPOS,range(BPOS,TRel),TMRan)).

alloy_to_b_special_multiplicity_type(partial_surjection, BPOS, _, TMDom, TMRan, partial_surjection(BPOS,TMDom,TMRan), none, no).

alloy_to_b_special_multiplicity_type(total_surjection, BPOS, _, TMDom, TMRan, total_surjection(BPOS,TMDom,TMRan), none, no).

alloy_to_b_special_multiplicity_type(injection_relation, BPOS, _, TMDom, TMRan, partial_function(BPOS,TMRan,TMDom), none, yes).

alloy_to_b_special_multiplicity_type(injection_surjection_relation, BPOS, _, TMDom, TMRan, partial_surjection(BPOS,TMRan,TMDom), none, yes).

alloy_to_b_special_multiplicity_type(partial_injection, BPOS, _, TMDom, TMRan, partial_injection(BPOS,TMDom,TMRan), none, no).

alloy_to_b_special_multiplicity_type(total_injection, BPOS, _, TMDom, TMRan, total_injection(BPOS,TMDom,TMRan), none, no).

alloy_to_b_special_multiplicity_type(bijection_relation, BPOS, _, TMDom, TMRan, total_function(BPOS,TMRan,TMDom), none, yes).

alloy_to_b_special_multiplicity_type(total_bijection_relation, BPOS, _, TMDom, TMRan, total_surjection(BPOS,TMRan,TMDom), none, yes).

alloy_to_b_special_multiplicity_type(partial_bijection, BPOS, _, TMDom, TMRan, partial_bijection(BPOS,TMDom,TMRan), none, no).

alloy_to_b_special_multiplicity_type(total_bijection, BPOS, _, TMDom, TMRan, total_bijection(BPOS,TMDom,TMRan), none, no).

alloy_to_b_unary_operator(not, negation).

alloy_to_b_unary_operator(closure1, closure).

alloy_to_b_unary_operator(closure, reflexive_closure).

alloy_to_b_unary_operator(inverse, reverse). % works for binary relation only; indeed Alloy says: ~ can be used only with a binary relation.

annotate_undefined_ordering_definition_call(Atom, _, Out) :-
    atom(Atom),
    !,
    Out = Atom.

annotate_undefined_ordering_definition_call(join(Arg1,Arg2,Type,POS), AnnotateWith, Annotated) :-
    is_ordering_definition_call(Arg1),
    !,
    annotate_undefined_ordering_definition_call(Arg2, AnnotateWith, NArg2),
    Annotated = join(Arg1,NArg2,Type,POS).

annotate_undefined_ordering_definition_call(join(Arg1,Arg2,Type,POS), AnnotateWith, Annotated) :-
    is_ordering_definition_call(Arg2),
    !,
    annotate_undefined_ordering_definition_call(Arg1, AnnotateWith, NArg1),
    Annotated = join(NArg1,Arg2,Type,POS).

annotate_undefined_ordering_definition_call(Binary, AnnotateWith, Annotated) :-
    % TODO: nested join with different top-level ordering definition call here?
    functor(Binary, BFun, 4),
    !,
    arg(1, Binary, Arg1),
    arg(2, Binary, Arg2),
    arg(3, Binary, Type),
    arg(4, Binary, POS),
    ( is_ordering_definition_call(Arg1)
    -> get_alloy_position(Arg1, A1POS),
    get_alloy_type(Arg1, Arg1Type),
    NArg1 = join(AnnotateWith,Arg1,Arg1Type,A1POS)
    ; annotate_undefined_ordering_definition_call(Arg1, AnnotateWith, NArg1)
    ),
    ( is_ordering_definition_call(Arg2)
    -> get_alloy_position(Arg2, A2POS),
    get_alloy_type(Arg2, Arg2Type),
    NArg2 = join(AnnotateWith,Arg2,Arg2Type,A2POS)
    ; annotate_undefined_ordering_definition_call(Arg2, AnnotateWith, NArg2)
    ),
    functor(Annotated, BFun, 4),
    arg(1, Annotated, NArg1),
    arg(2, Annotated, NArg2),
    arg(3, Annotated, Type),
    arg(4, Annotated, POS).

annotate_undefined_ordering_definition_call(AlloyTerm, _, AlloyTerm).

assert_abstract_sig(Options, Name) :-
    member(abstract, Options),
    !,
    asserta(abstract_sig(Name)).

assert_abstract_sig(_, _).

assert_artificial_parent_types(SetOfTypeSets) :-
    assert_artificial_parent_types(0, SetOfTypeSets).

assert_artificial_parent_types(_, []).

assert_artificial_parent_types(C, [SetOfTypes|T]) :-
    gen_identifier(C, "_universe", ParentId),
    gen_identifier(C, "_Universe", PParentId),
    C1 is C + 1,
    assert_parent_id_for_types(SetOfTypes, ParentId, PParentId),
    assert_artificial_parent_types(C1, T).

assert_atelierb_mode :-
    get_preference(alloy_translation_for_proof, true),
    !,
    temporary_set_preference(translate_print_typing_infos, true),
    translate:set_atelierb_mode(native).

assert_atelierb_mode.

assert_current_module_in_scope(ModuleName, Alias) :-
    module_in_scope_but_root(ModuleName, Alias),
    retractall(current_module_in_scope(_)),
    asserta(current_module_in_scope(ModuleName)).

assert_current_module_in_scope(_, _).

assert_enumerated_set(Options, Name) :-
    % singleton top-level signatures are defined as an enumerated set like S = {_S}
    member(one, Options),
    % but extending singleton signatures are defined as constants and singleton subsets of their parent type
    \+ member(subset(_), Options),
    \+ member(subsig(_), Options),
    !,
    asserta(enumerated_set(Name)).

assert_enumerated_set(_, _).

assert_extending_signature(Name, Parent, One) :-
    ( is_sub_signature_of(Name, Parent, One) ->
    true
    ; debug_format(19, '~w is sub signature of ~w (~w)~n', [Name,Parent,One]),
    assertz(is_sub_signature_of(Name, Parent, One))
    ),
    extending_signatures(List),
    select((Parent,SubSigs), List, Rest),
    !,
    ( \+ memberchk(Name/One, SubSigs)
    ->
    retractall(extending_signatures(_)),
    asserta(extending_signatures([(Parent,[Name/One|SubSigs])|Rest]))
    ; true
).

assert_extending_signature(Name, Parent, One) :-
    retract(extending_signatures(List)),
    !,
    asserta(extending_signatures([(Parent,[Name/One])|List])).

assert_extending_signature(Name, Parent, One) :-
    asserta(extending_signatures([(Parent,[Name/One])])).

assert_integer_type_from_preference :-
    get_preference(alloy_use_implementable_integers, Pref),
    retractall(integer_type(_)),
    retractall(natural_type(_)),
    ( Pref == true
    -> asserta(integer_type('INT')),
    asserta(natural_type('NAT'))
    ; asserta(integer_type('INTEGER')),
    asserta(natural_type('NATURAL'))
).

assert_ordered_sig_name(Name) :-
    asserta(ordered_signature(Name)).

assert_parent_id_for_types([], _, _).

assert_parent_id_for_types([SignatureName|T], ParentId, PParentId) :-
    asserta(artificial_parent_type(SignatureName,ParentId,PParentId)),
    assert_parent_id_for_types(T, ParentId, PParentId).

assert_singleton_set(Name) :- % debug_format(19,'Singleton set : ~w~n',[Name]),nl,
    % \+ singleton_set(Name),
    asserta(singleton_set(Name)),
    !.

assert_singleton_set(Options, Name) :-
    member(one, Options),
    !,
    assert_singleton_set(Name).

assert_singleton_set(_, _).

assert_total_function(identifier(_,Name), SIG) :-
    !,
    assert_total_function(Name, SIG).

assert_total_function(Name, identifier(_,SIG)) :-
    !,
    assert_total_function(Name, SIG).

assert_total_function(Name, SIG) :-
    debug_format(19, 'Total function ~w over ~w~n', [Name,SIG]),
    asserta(total_function(Name, SIG)).

atom_ends_with(Atom, EndsWith) :-
    atom_concat(_, EndsWith, Atom).

binary_op_not_allowing_iden_or_univ(equal).

binary_op_not_allowing_iden_or_univ(not_equal).

binary_op_not_allowing_iden_or_univ(in).

binary_op_not_allowing_iden_or_univ(not_in).

build_machine_ast(b_machine(ListOfMachineParts,_SignatureNames), machine(generated(none,AbstractMachine))) :-
    % filter empty machine parts
    findall(MachinePart, ( member(MachinePart, ListOfMachineParts),
    arg(2,MachinePart,L),
    L \== []
    ), NonEmptyMachineSections),
    % properties need to be conjoined
    ( select(properties(none,L), NonEmptyMachineSections, RestListOfUsedMachineParts) ->
    true
    ; L == [],
    RestListOfUsedMachineParts = NonEmptyMachineSections
    ),
    join_predicates(conjunct, L, FlatL),
    AbstractMachine = abstract_machine(none,machine(none),
    machine_header(none,alloytranslation,[]),
    [properties(none,FlatL)|RestListOfUsedMachineParts]),
    !.

calculate_max_parent_type_card(SigNames, GlobalScope, ExactScopes, UpBoundScopes, MaxCard) :-
    calculate_max_parent_type_card(SigNames, GlobalScope, ExactScopes, UpBoundScopes, 0, MaxCard).

calculate_max_parent_type_card([], _, _, _, Acc, Acc).

calculate_max_parent_type_card([SigName|T], GlobalScope, ExactScopes, UpBoundScopes, Acc, MaxCard) :-
    ( (member((SigName,Scope), ExactScopes); member((SigName,Scope), UpBoundScopes))
    -> NAcc is Acc + Scope
    ; NAcc is Acc + GlobalScope
    ),
    calculate_max_parent_type_card(T, GlobalScope, ExactScopes, UpBoundScopes, NAcc, MaxCard).

can_remove_singleton_set(set_extension(_,[Element]), Element).

check_position(Var,PP) :- var(Var),!,add_internal_error('Variable position at: ',PP),Var=none.

check_position(P,_) :- is_valid_position(P),!.

check_position(T,PP) :- add_warning(check_position,'Unknown position at: ',PP:T).

check_valid_raw_translation(_,_).

construct_all_diff(BPOS,2,[S1,S2],AllDiff) :- !, AllDiff = not_equal(BPOS,S1,S2).

construct_all_diff(BPOS,Len,TSets, AllDiff) :-
    AllDiff = equal(BPOS,card(BPOS,general_union(BPOS,set_extension(BPOS,TSets))),integer(BPOS,Len)).

create_cartesian_type([ID], TID) :-
    !,
    translate_unary_e_p(ID, TID).

create_cartesian_type([ID1,ID2], cartesian_product(none,TID1,TID2)) :-
    !,
    translate_unary_e_p(ID1, TID1),
    translate_unary_e_p(ID2, TID2).

create_cartesian_type([ID1,ID2|T], cartesian_product(none,cartesian_product(none,TID1,TID2),NT)) :-
    translate_unary_e_p(ID1, TID1),
    translate_unary_e_p(ID2, TID2),
    create_cartesian_type(T, NT).

default_max_seq(7).

default_upper_bound_scope(3).

define_artificial_parent_types(MAcc, [], MAcc, _, _, _).

define_artificial_parent_types(MAcc, [(ParentId,PParentId)|T], NewMAcc, GlobalScope, ExactScopes, UpBoundScopes) :-
    PParentId = identifier(_,PParentName),
    findall(SigName, artificial_parent_type(SigName,ParentId,_), DSigNames),
    DSigNames \== [],
    remove_dups(DSigNames, SigNames),
    maplist(translate_e_p, SigNames, TSigNames),
    % should be: _universe0 = S1 \/ .. \/ Sn
    % ProB currently does not set the deferred set size of P0 in cbc mode if it is defined within an operation's precondition
    % (ProB uses the preference 'deferred_setsize' which then might be a contradiction)
    % this equality is valid if it is translated in the properties and not as a precondition which is the case
    % if we only translate a single run or check command
    % _universe0 = S1 \/ .. \/ Sn
    join_untyped_ast_nodes(union, TSigNames, Union),
    ParentDomain = equal(none,ParentId,Union),
    % TO DO: use above code if this issue is solved, otherwise stick to this translation which is just less performant in case we do not constrain _P0
    % if we constrain _P0, e.g., using id(_P0), this could be an error as _P0 possibly contains more elements than necessary
    % Note: if preference 'deferred_setsize' is smaller than n, this is still a contradiction
    % S1 \/ .. \/ Sn <: universe0
    %join_untyped_ast_nodes(union, TSigNames, Union),
    %ParentDomain = subset(none, Union, ParentId),
    extend_machine_acc(properties, MAcc, ParentDomain, MAcc1),
    calculate_max_parent_type_card(SigNames, GlobalScope, ExactScopes, UpBoundScopes, MaxCard),
    % _universe0 <: _Universe0 & card(_Universe0) = MaxCard
    Subset = subset(none,ParentId,PParentId),
    CardEq = equal(none,card(none,PParentId),integer(none,MaxCard)),
    extend_machine_acc(properties, MAcc1, conjunct(none,Subset,CardEq), MAcc2),
    % S1 /\ S2 = {} & .. & Sn-1 /\ Sn = {}
    disjoint_set_of_signatures(TSigNames, DisjointConstraint),
    extend_machine_acc(properties, MAcc2, DisjointConstraint, MAcc3),
    extend_machine_acc(constants, MAcc3, ParentId, MAcc4),
    extend_machine_acc(sets, MAcc4, deferred_set(none,PParentName), MAcc5),
    define_artificial_parent_types(MAcc5, T, NewMAcc, GlobalScope, ExactScopes, UpBoundScopes).

define_artificial_parent_types_if_necessary(MAcc, NewMAcc, GlobalScope, ExactScopes, UpBoundScopes) :-
    findall((ParentId,PParentId), artificial_parent_type(_, ParentId, PParentId), TParents),
    remove_dups(TParents, Parents),
    define_artificial_parent_types(MAcc, Parents, NewMAcc, GlobalScope, ExactScopes, UpBoundScopes).

define_ordered_signature_as_integer_set(OrdSigCounter, TSignatureName, Scope, TScope, NewOrdSigCounter) :-
    NewOrdSigCounter is OrdSigCounter+Scope,
    UpBound is NewOrdSigCounter-1,
    % TSignatureName = OrdSigCounter...UpBound
    TScope = equal(none,identifier(none,TSignatureName),
    interval(none,integer(none,OrdSigCounter),integer(none,UpBound))).

define_ordered_signature_functions(POS, MAcc, Sig, NewMAcc) :-
    translate_pos(POS, BPOS),
    gen_identifier(0, "_c_", TIDX),
    TIDS = identifier(BPOS,s),
    translate_e_p(Sig, TSig),
    MemberX = member(BPOS,TIDX,TSig),
    % next_Sig(s) == IF succ[s] <: Sig THEN succ[s] ELSE {} END
    atom_concat(next_, Sig, NextName),
    SuccessorImg = image(BPOS,successor(BPOS),TIDS),
    PredecessorImg = image(BPOS,predecessor(BPOS),TIDS),
    extend_machine_acc(definitions, MAcc,
    expression_definition(BPOS,NextName,[TIDS],if_then_else(BPOS,subset(BPOS,SuccessorImg,TSig),SuccessorImg,empty_set(BPOS))), MAcc1),
    % nexts_Sig(s) == {x|x:Sig & min({x} \/ s) /= x}
    atom_concat(nexts_, Sig, NextsName),
    NextsBody = conjunct(BPOS,MemberX,not_equal(BPOS,min(BPOS,union(BPOS,set_extension(BPOS,[TIDX]),TIDS)),TIDX)),
    extend_machine_acc(definitions, MAcc1,
    expression_definition(BPOS,NextsName,[TIDS],comprehension_set(BPOS,[TIDX],NextsBody)), MAcc2),
    atom_concat(prev_, Sig, PrevName),
    % prev_Sig(s) == IF pred[s] <: Sig THEN pred[s] ELSE {} END
    extend_machine_acc(definitions, MAcc2,
    expression_definition(BPOS,PrevName,[TIDS],if_then_else(BPOS,subset(BPOS,PredecessorImg,TSig),PredecessorImg,empty_set(BPOS))), MAcc3),
    % prevs_Sig(s) == {x|x:Sig & max({x} \/ s) /= x}
    atom_concat(prevs_, Sig, PrevsName),
    PrevsBody = conjunct(BPOS,MemberX,not_equal(BPOS,max(BPOS,union(BPOS,set_extension(BPOS,[TIDX]),TIDS)),TIDX)),
    extend_machine_acc(definitions, MAcc3,
    expression_definition(BPOS,PrevsName,[TIDS],comprehension_set(BPOS,[TIDX],PrevsBody)), NewMAcc).

define_ordered_signatures_as_integer_set([], OrdSigCounter, _, [], OrdSigCounter).

define_ordered_signatures_as_integer_set([TSignatureName|T], OrdSigCounter, Scope, [TScope|TScopes], NewOrdSigCounter) :-
    define_ordered_signature_as_integer_set(OrdSigCounter, TSignatureName, Scope, TScope, OrdSigCounter1),
    define_ordered_signatures_as_integer_set(T, OrdSigCounter1, Scope, TScopes, NewOrdSigCounter).

define_sig_as_set_or_constant(MAcc, Name, Options, POS, NewMAcc) :-
    memberchk(subset(Parents), Options),
    !,
    % maplist(assert_extending_signature(Name),Parents) , % subset signatures do not need to be distinct
    translate_pos(POS, BPOS),
    define_sig_as_set_or_constant_aux(constants, MAcc, Name, Options, BPOS, MAcc1),
    % TO DO: consider several parents -> we need the universe type
    Parents = [Parent|_],
    translate_e_p(Name, TName),
    translate_e_p(Parent, TParent),
    TNode = subset(BPOS,TName,TParent),
    extend_machine_acc(properties, MAcc1, TNode, NewMAcc).

define_sig_as_set_or_constant(MAcc, Name, Options, POS, NewMAcc) :-
    member(subsig(Parent), Options),
    !,
    ( member(one, Options) ->
    One = one
    ; One = set
    ),
    assert_extending_signature(Name, Parent, One),
    translate_pos(POS, BPOS),
    define_sig_as_set_or_constant_aux(constants, MAcc, Name, Options, BPOS, MAcc1),
    translate_e_p(Name, TName),
    translate_e_p(Parent, TParent),
    TNode = subset(BPOS,TName,TParent),
    extend_machine_acc(properties, MAcc1, TNode, NewMAcc).

define_sig_as_set_or_constant(MAcc, Name, Options, POS, NewMAcc) :-
    translate_pos(POS, BPOS),
    artificial_parent_type(Name, ParentId, _),
    !,
    translate_e_p(Name, TName),
    TNode = subset(BPOS,TName,ParentId),
    extend_machine_acc(properties, MAcc, TNode, MAcc1),
    define_sig_as_set_or_constant_aux(constants, MAcc1, Name, Options, BPOS, NewMAcc).

define_sig_as_set_or_constant(MAcc, Name, Options, POS, NewMAcc) :-
    translate_pos(POS, BPOS),
    define_sig_as_set_or_constant_aux(sets, MAcc, Name, Options, BPOS, NewMAcc).

define_sig_as_set_or_constant_aux(sets, MAcc, Name, Options, BPOS, NewMAcc) :-
    member(one, Options),
    !,
    atom_concat('_', Name, EnumElement),
    % TO DO: couldn't figure out untyped ast of enumerated set, define enumerated set S = {_S} instead of constant etc.
    extend_machine_acc(sets, MAcc, deferred_set(BPOS,Name), MAcc1),
    extend_machine_acc(constants, MAcc1, identifier(BPOS,EnumElement), MAcc2),
    extend_machine_acc(properties, MAcc2, equal(BPOS,identifier(BPOS,Name),set_extension(BPOS,[identifier(BPOS,EnumElement)])), NewMAcc).

define_sig_as_set_or_constant_aux(sets, MAcc, Name, Options, BPOS, NewMAcc) :-
    member(some, Options),
    !,
    extend_machine_acc(sets, MAcc, deferred_set(BPOS,Name), MAcc1),
    extend_machine_acc(properties, MAcc1, greater_equal(BPOS,card(BPOS,identifier(BPOS,Name)),integer(BPOS,1)), NewMAcc).

define_sig_as_set_or_constant_aux(sets, MAcc, Name, Options, BPOS, NewMAcc) :-
    member(lone, Options),
    !,
    extend_machine_acc(sets, MAcc, deferred_set(BPOS,Name), MAcc1),
    extend_machine_acc(properties, MAcc1, less_equal(BPOS,card(BPOS,identifier(BPOS,Name)),integer(BPOS,1)), NewMAcc).

define_sig_as_set_or_constant_aux(sets, MAcc, Name, _Options, BPOS, NewMAcc) :-
    extend_machine_acc(sets, MAcc, deferred_set(BPOS,Name), NewMAcc).

define_sig_as_set_or_constant_aux(constants, MAcc, Name, _Options, BPOS, NewMAcc) :-
    extend_machine_acc(constants, MAcc, identifier(BPOS,Name), NewMAcc).