| 1 | % (c) 2017-2019 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
| 2 | % Heinrich Heine Universitaet Duesseldorf | |
| 3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
| 4 | ||
| 5 | :- module(alloy2b,[load_alloy_ast_prolog_file/1, | |
| 6 | load_alloy_model/2, | |
| 7 | load_alloy_model/3, | |
| 8 | translate_alloy_model/2]). | |
| 9 | ||
| 10 | :- use_module(probsrc(debug)). | |
| 11 | :- use_module(library(lists)). | |
| 12 | :- use_module(library(plunit)). | |
| 13 | :- use_module(probsrc(bmachine)). | |
| 14 | :- use_module(probsrc(translate)). | |
| 15 | :- use_module(library(file_systems)). | |
| 16 | :- use_module(probsrc(error_manager)). | |
| 17 | :- use_module(library(sets),[subtract/3]). | |
| 18 | :- use_module(probsrc(specfile),[set_animation_minor_mode/1]). | |
| 19 | :- use_module(library(ordsets),[ord_intersection/3, ord_union/3, ord_subtract/3]). | |
| 20 | ||
| 21 | :- dynamic enumerated_set/1, singleton_set/1, total_function/2, ordered_signature/1, command_counter/1, extending_signatures/1, is_sub_signature_of/3, is_seq/1, current_command/1, maxseq/1, uses_seqs/0. | |
| 22 | :- volatile enumerated_set/1, singleton_set/1, total_function/2, ordered_signature/1, command_counter/1, extending_signatures/1, is_sub_signature_of/3, is_seq/1, current_command/1, maxseq/1, uses_seqs/0. | |
| 23 | ||
| 24 | :- meta_predicate map_translate(3,-,-,-). | |
| 25 | ||
| 26 | command_counter(0). | |
| 27 | ||
| 28 | % An automated translation from Alloy to classical B. | |
| 29 | % The Alloy abstract syntax tree is translated to an untyped B AST as supported by ProB. | |
| 30 | % Afterwards, the untyped AST can be typechecked and loaded by ProB. | |
| 31 | % The used positions are from the Alloy parser and thus refer to the Alloy model. | |
| 32 | ||
| 33 | % Usage: | |
| 34 | % load_alloy_model/2: input is an Alloy model represented as a Prolog term as provided by the Kotlin translation; the model is translated to an untyped B AST and loaded by ProB | |
| 35 | % translate_alloy_model/2: input is an Alloy model represented as a Prolog term as provided by the Kotlin translation, output is an untyped B AST | |
| 36 | ||
| 37 | % Run tests: | |
| 38 | % - launch ProB Tcl/Tk or ProB CLI | |
| 39 | % - 'use_module(extension('alloy2b/alloy2b')).' | |
| 40 | % - 'error_manager:reset_errors , plunit:run_tests(full_machine_translation).'. | |
| 41 | % - run a single test: 'error_manager:reset_errors , plunit:run_tests(full_machine_translation:directctrl).' | |
| 42 | % - 'bmachine:full_b_machine(L) , translate:print_machine(L)'. | |
| 43 | ||
| 44 | % KNOWN ISSUES / TO DOs | |
| 45 | % ---------------------- | |
| 46 | % - nested quantifiers: the usage of facts for singleton_set is error prone, and cannot deal with | |
| 47 | % nested quantifiers with variable clashes, in particular when in the inner quantifier the | |
| 48 | % identifier is not a singleton set | |
| 49 | % - multiplicity annotations in signatures and nested multiplicity annotations for non-binary relations | |
| 50 | % - variable capture due to use of DEFINITIONS | |
| 51 | % - ProB does not allow arithmetic operators on non-singleton sets; | |
| 52 | % this is a design decision to detect most probably unintended uses of arithmetic | |
| 53 | % - ProB does use mathematical integers, bit-width is used for MAXINT and MININT, but only influences | |
| 54 | % enumeration scopes | |
| 55 | ||
| 56 | load_alloy_ast_prolog_file(File) :- | |
| 57 | \+ file_exists(File,read) , ! , | |
| 58 | add_error(load_alloy_ast_prolog_file,'Alloy AST file has not been created:',[File]) , fail. | |
| 59 | load_alloy_ast_prolog_file(File) :- | |
| 60 | format('Opening Alloy AST file: ~w~n',[File]), | |
| 61 | open(File,read,Stream), | |
| 62 | safe_read_term(Stream,AlloyTerm), | |
| 63 | close(Stream), | |
| 64 | load_alloy_model(AlloyTerm,'alloytranslation'). | |
| 65 | ||
| 66 | safe_read_term(Stream,Term) :- | |
| 67 | on_exception(error(E,_), read(Stream,Term), | |
| 68 | (add_internal_error('Exception while reading Prolog term from stream:',E), | |
| 69 | fail)). | |
| 70 | ||
| 71 | load_alloy_model(AlloyTerm,AlloyFile) :- | |
| 72 | % use the first run or check command by default for models that use sequences, otherwise all commands are translated | |
| 73 | load_alloy_model(0,AlloyTerm,AlloyFile). | |
| 74 | ||
| 75 | load_alloy_model(CurrentCommand,AlloyTerm,AlloyFile) :- | |
| 76 | integer(CurrentCommand) , | |
| 77 | reset_errors , | |
| 78 | format('Translating AST to B.~n',[]) , | |
| 79 | retract_state, % in case things not properly reseted or initialised | |
| 80 | assert(current_command(CurrentCommand)) , | |
| 81 | %tools_printing:nested_print_term(AlloyTerm,10), | |
| 82 | translate_alloy_model(AlloyTerm,UntypedBAst) , ! , | |
| 83 | UntypedBAst = machine(generated(none,AbstractMachine)) , | |
| 84 | b_load_machine_from_term(AlloyFile,complete_machine('alloytranslation',[AbstractMachine],[AlloyFile])), | |
| 85 | set_animation_minor_mode(alloy). | |
| 86 | load_alloy_model(CurrentCommand,_,_) :- | |
| 87 | \+ integer(CurrentCommand) , | |
| 88 | add_error(load_alloy_model,'Current command has to be an integer:',CurrentCommand) , fail. | |
| 89 | load_alloy_model(_,AlloyTerm,_) :- | |
| 90 | add_error(load_alloy_model,'Translating Alloy AST failed:',AlloyTerm) , fail. | |
| 91 | ||
| 92 | process_options(Options) :- | |
| 93 | member(sequences:B,Options) , | |
| 94 | B == true , ! , | |
| 95 | asserta(uses_seqs). | |
| 96 | process_options(_). | |
| 97 | ||
| 98 | % TODO: handle all modules in the model but exclude integer, relation, ordering and sequences | |
| 99 | % Currently we only extract and translate the main module | |
| 100 | translate_alloy_model(alloy(RootModule, Models), UntypedBAst) :- | |
| 101 | member(alloy_model(RootModule,Facts,Assertions,Commands,Functions,Signatures,OSigNames,Options),Models),!, | |
| 102 | translate_alloy_model(alloy_model(RootModule,Facts,Assertions,Commands,Functions,Signatures,OSigNames,Options), UntypedBAst). | |
| 103 | ||
| 104 | % TODO: use atelierb_pp_mode (e.g. we use let expressions which are not supported by native B) | |
| 105 | translate_alloy_model(alloy_model(_ModuleName, facts(Facts),assertions(Assertions),commands(Commands),functions(Functions), | |
| 106 | signatures(Signatures),ordered_signatures(OSigNames),Options),UntypedBAst) :- | |
| 107 | % singleton sets are asserted at runtime using singleton_set/1 | |
| 108 | % accumulate all translations, afterwards we build the untyped machine ast | |
| 109 | process_options(Options) , | |
| 110 | maplist(assert_ordered_sig_name,OSigNames) , | |
| 111 | empty_machine_acc(MAcc), | |
| 112 | debug_println(19,translating_signatures), | |
| 113 | maplist(preprocess_signature,Signatures), % assert some signature names as singleton | |
| 114 | map_translate(translate_signature,MAcc,Signatures,MAcc0), | |
| 115 | debug_println(19,translating_assertions), | |
| 116 | map_translate(translate_assertion,MAcc0,Assertions,MAcc1), | |
| 117 | debug_println(19,translating_commands), | |
| 118 | % TO DO: extract common scopes for all commands, to set deferred set sizes: | |
| 119 | % NOTE: extract_common_scopes can be removed in case we stick to translating a single command at a time | |
| 120 | extract_common_scopes(Commands,GS,ExactScopes,UpBoundScopes,BitWidth,TMaxSeq,Con), | |
| 121 | (TMaxSeq = maxSeq(MaxSeq) ; MaxSeq = -1) , | |
| 122 | format('Common scopes to all commands : global=~w, exact=~w, bw=~w, ms=~w, conflicts=~w~n',[GS,ExactScopes,BitWidth,MaxSeq,Con]), | |
| 123 | (number(GS),GS>0 -> preferences:temporary_set_preference(globalsets_fdrange,GS) % TO DO: improve | |
| 124 | ; true), | |
| 125 | maplist(generate_exact_scope_predicate,ExactScopes,ScopePreds1), | |
| 126 | maplist(generate_leq_scope_predicate,UpBoundScopes,ScopePreds2), | |
| 127 | append(ScopePreds1,ScopePreds2,ScopePreds), | |
| 128 | extend_machine_with_conjuncts(properties,ScopePreds,MAcc1,MAcc2), | |
| 129 | (BitWidth=bitwidth(BW), number(BW), BW>0, | |
| 130 | MaxInt is integer(2**(BW-1)) -1, MinInt is integer(-(2**(BW-1))), | |
| 131 | preferences:temporary_set_preference(maxint,MaxInt), | |
| 132 | preferences:temporary_set_preference(minint,MinInt) | |
| 133 | -> true ; true), | |
| 134 | (MaxSeq \= -1 | |
| 135 | -> translate_seq_scopes(MaxSeq,SeqScopesPred) , extend_machine_acc(properties,MAcc2,SeqScopesPred,MAcc3) | |
| 136 | ; MAcc3 = MAcc2) , | |
| 137 | map_translate(translate_command,MAcc3,Commands,MAcc4) , | |
| 138 | debug_println(19,translating_functions), | |
| 139 | map_translate(translate_function,MAcc4,Functions,MAcc5) , | |
| 140 | debug_println(19,translating_facts), | |
| 141 | map_translate(translate_fact,MAcc5,Facts,MAcc6) , ! , | |
| 142 | finalize_extending_signatures(MAcc6,MAcc7) , | |
| 143 | debug_println(19,build_machine_ast), | |
| 144 | build_machine_ast(MAcc7,UntypedBAst), | |
| 145 | %print(UntypedBAst),nl,nl, | |
| 146 | %tools_printing:nested_print_term(UntypedBAst,20), | |
| 147 | (debug_mode(off) -> true ; nl,translate:print_raw_machine_terms(UntypedBAst),nl), | |
| 148 | retract_state. | |
| 149 | ||
| 150 | map_translate(_,MAcc,[],MAcc). | |
| 151 | map_translate(TypePred,MAcc,[Part|T],Res) :- | |
| 152 | call(TypePred,MAcc,Part,NewMAcc) , | |
| 153 | map_translate(TypePred,NewMAcc,T,Res). | |
| 154 | ||
| 155 | % things that need to be done before translating the signatures, e.g., assert singleton set info | |
| 156 | preprocess_signature(signature(Name,_Fields,_Facts,Options,_)) :- | |
| 157 | % assert signatures for singleton checks | |
| 158 | assert_singleton_set(Options,Name) , | |
| 159 | assert_enumerated_set(Options,Name). | |
| 160 | ||
| 161 | % translate signature declaration sig Name {Fields} | |
| 162 | translate_signature(MAcc,signature(Name,Fields,Facts,Options,pos(Col,Row)),NewMAcc) :- | |
| 163 | extend_machine_acc(signatures,MAcc,[Name],MAcc1), | |
| 164 | translate_signature_aux(Name,Options,pos(Col,Row),MAcc1,MAcc2), | |
| 165 | translate_signature_fields(Fields,Name,MAcc2,MAcc3), | |
| 166 | translate_e_p(Name,TName) , | |
| 167 | map_translate(translate_signature_fact(TName),MAcc3,Facts,NewMAcc). | |
| 168 | ||
| 169 | translate_signature_aux(Name,Options,Pos,MAcc,NewMAcc) :- | |
| 170 | % ordered signatures are defined as distinct sets of integer when translating a command | |
| 171 | member(ordered,Options) , ! , | |
| 172 | define_ordered_signature_functions(Pos,MAcc,Name,MAcc1) , | |
| 173 | extend_machine_acc(signatures,MAcc1,[Name],MAcc2) , | |
| 174 | translate_e_p(Name,TID) , | |
| 175 | extend_machine_acc(properties,MAcc2, | |
| 176 | member(none,TID,pow_subset(none,integer_set(none,'INTEGER'))),MAcc3) , | |
| 177 | define_sig_as_set_or_constant_aux(constants,MAcc3,Name,Options,Pos,NewMAcc). | |
| 178 | translate_signature_aux(Name,Options,Pos,MAcc,NewMAcc) :- | |
| 179 | define_sig_as_set_or_constant(MAcc,Name,Options,Pos,NewMAcc). | |
| 180 | ||
| 181 | define_ordered_signature_functions(POS,MAcc,Sig,NewMAcc) :- | |
| 182 | translate_pos(POS,BPOS), | |
| 183 | gen_identifier(0,"_c_",TIDX), | |
| 184 | TIDS = identifier(BPOS,s) , | |
| 185 | translate_e_p(Sig,TSig) , MemberX = member(BPOS,TIDX,TSig) , | |
| 186 | % next_Sig(s) == IF succ[s] <: Sig THEN succ[s] ELSE {} END | |
| 187 | atom_concat(next_,Sig,NextName) , | |
| 188 | SuccessorImg = image(BPOS,successor(BPOS),TIDS) , | |
| 189 | PredecessorImg = image(BPOS,predecessor(BPOS),TIDS) , | |
| 190 | extend_machine_acc(definitions,MAcc, | |
| 191 | expression_definition(BPOS,NextName,[TIDS],if_then_else(BPOS,subset(BPOS,SuccessorImg,TSig),SuccessorImg,empty_set(BPOS))),MAcc1) , | |
| 192 | % nexts_Sig(s) == {x|x:Sig & min({x} \/ s) /: {x}} | |
| 193 | atom_concat(nexts_,Sig,NextsName) , | |
| 194 | NextsBody = conjunct(BPOS,MemberX,not_member(BPOS,min(BPOS,union(BPOS,set_extension(BPOS,[TIDX]),TIDS)),set_extension(BPOS,[TIDX]))) , | |
| 195 | extend_machine_acc(definitions,MAcc1, | |
| 196 | expression_definition(BPOS,NextsName,[TIDS],comprehension_set(BPOS,[TIDX],NextsBody)),MAcc2) , | |
| 197 | atom_concat(prev_,Sig,PrevName) , | |
| 198 | % prev_Sig(s) == IF pred[s] <: Sig THEN pred[s] ELSE {} END | |
| 199 | extend_machine_acc(definitions,MAcc2, | |
| 200 | expression_definition(BPOS,PrevName,[TIDS],if_then_else(BPOS,subset(BPOS,PredecessorImg,TSig),PredecessorImg,empty_set(BPOS))),MAcc3) , | |
| 201 | % prevs_Sig(s) == {x|x:Sig & max({x} \/ s) /: {x}} | |
| 202 | atom_concat(prevs_,Sig,PrevsName) , | |
| 203 | PrevsBody = conjunct(BPOS,MemberX,not_member(BPOS,max(BPOS,union(BPOS,set_extension(BPOS,[TIDX]),TIDS)),set_extension(BPOS,[TIDX]))) , | |
| 204 | extend_machine_acc(definitions,MAcc3, | |
| 205 | expression_definition(BPOS,PrevsName,[TIDS],comprehension_set(BPOS,[TIDX],PrevsBody)),NewMAcc). | |
| 206 | ||
| 207 | translate_signature_fields(Fields,SignatureName) --> | |
| 208 | {translate_e_p(SignatureName,TSignatureName)}, | |
| 209 | translate_signature_fields_aux(Fields,SignatureName,TSignatureName). | |
| 210 | ||
| 211 | translate_signature_fields_aux([],_,_) --> []. | |
| 212 | translate_signature_fields_aux([Field|T],SignatureName,TSignatureName) --> | |
| 213 | translate_signature_field(SignatureName,TSignatureName,Field), | |
| 214 | translate_signature_fields_aux(T,SignatureName,TSignatureName). | |
| 215 | ||
| 216 | translate_signature_field(SignatureName,TSignatureName,Field,MAcc,NewMAcc) :- | |
| 217 | translate_signature_field_aux(SignatureName,TSignatureName,Field,TField,MAcc,MAcc1), | |
| 218 | extend_machine_acc(properties,MAcc1,TField,NewMAcc). | |
| 219 | ||
| 220 | translate_signature_field_aux(SignatureName,TSignatureName, | |
| 221 | field(FieldName,Expr,FieldType,Options,POS),TFieldPred,MAcc,NewMAcc) :- | |
| 222 | FieldType = type(TypeList,Arity), A1 is Arity+1, % add SignatureName to type: | |
| 223 | FieldID = identifier(FieldName,type([SignatureName|TypeList],A1),POS), | |
| 224 | translate_e_p(FieldName,TFieldName), | |
| 225 | extend_machine_acc(constants,MAcc,TFieldName,MAcc1) , | |
| 226 | translate_pos(POS,BPOS), | |
| 227 | disjoint_field_declaration(TSignatureName,BPOS,Options,MAcc1,TFieldName,NewMAcc) , | |
| 228 | translate_field_decl(BPOS,SignatureName,TSignatureName,Expr,FieldID,TFieldName,TFieldPred) , !. | |
| 229 | ||
| 230 | translate_function_field(field(FieldName,Expr,type(_Type,_Arity),_Options,POS),TField) :- | |
| 231 | %(Functor = function -> assert_singleton_set(FieldName) ; true) , % NO LONGER NEEDED | |
| 232 | translate_e_p(FieldName,TTFieldName), | |
| 233 | strip_singleton_set_from_this(TTFieldName,TFieldName) , % necessary for nested definition calls with 'this' | |
| 234 | translate_pos(POS,BPOS), | |
| 235 | fun_or_pred_decl_special_cases(Expr,TFieldName,BPOS,TField,_IsSingleton) , !. | |
| 236 | % TO DO: !! what if IsSingleton is set !! | |
| 237 | ||
| 238 | disjoint_field_declaration(TSignatureName,TPos,Options,MAcc,TFieldName,NewMAcc) :- | |
| 239 | member(disj,Options) , ! , | |
| 240 | % all a, b: S | a != b implies no a.f & b.f | |
| 241 | IdA = identifier(TPos,a) , IdB = identifier(TPos,b) , | |
| 242 | ImplLhs = conjunct(TPos,conjunct(TPos,member(TPos,IdA,TSignatureName),member(TPos,IdB,TSignatureName)), | |
| 243 | not_equal(TPos,IdA,IdB)) , | |
| 244 | ImplRhs = equal(TPos,intersection(TPos,image(TPos,TFieldName,set_extension(none,[IdA])), | |
| 245 | image(TPos,TFieldName,set_extension(none,[IdB]))),empty_set(TPos)) , | |
| 246 | Disjoint = forall(TPos,[IdA,IdB],implication(TPos,ImplLhs,ImplRhs)) , | |
| 247 | extend_machine_acc(properties,MAcc,Disjoint,NewMAcc). | |
| 248 | disjoint_field_declaration(_,_,_,MAcc,_,MAcc). | |
| 249 | ||
| 250 | ||
| 251 | ||
| 252 | is_disjoint_quantifier(Fields) :- Fields=[F|_], is_disjoint_quantifier_field(F). % assumption: all or no field is disjoint | |
| 253 | is_disjoint_quantifier_field(field(_FieldName,_Expr,type(_Type,_Arity),Options,_POS)) :- member(disj,Options). | |
| 254 | ||
| 255 | translate_quantifier_field(field(FieldName,Expr,type(_Type,_Arity),_Options,POS),TField,FieldName) :- | |
| 256 | translate_pos(POS,BPOS), | |
| 257 | fun_or_pred_decl_special_cases(Expr,TFieldName,BPOS,TField,IsSingleton), | |
| 258 | !, | |
| 259 | (IsSingleton=singleton -> | |
| 260 | assert_singleton_set(FieldName) ; true), | |
| 261 | translate_e_p(FieldName,TFieldName). | |
| 262 | ||
| 263 | ||
| 264 | translate_fact(MAcc,fact(Expr,_Pos),NewMAcc) :- | |
| 265 | translate_e_p(Expr,TExpr) , | |
| 266 | extend_machine_acc(properties,MAcc,TExpr,NewMAcc). | |
| 267 | translate_assertion(MAcc,fact(Expr,_Pos),NewMAcc) :- | |
| 268 | translate_e_p(Expr,TExpr) , | |
| 269 | extend_machine_acc(assertions,MAcc,TExpr,NewMAcc). | |
| 270 | ||
| 271 | % Signature facts: Identifiers may refer to the signature and are joined with 'this'. | |
| 272 | % We then need a universal quantification using 'this'. | |
| 273 | translate_signature_fact(TSignatureName,MAcc,Expr,NewMAcc) :- | |
| 274 | alloy_expr_contains_join(Expr), | |
| 275 | translate_e_p(Expr,TExpr), % we quantify in such a way that this is a singleton_set_id; this is always considered a singleton set id | |
| 276 | ThisID = identifier(none,'this'), | |
| 277 | TImplication = implication(none,subset(none,set_extension(none,[ThisID]),TSignatureName),TExpr), | |
| 278 | FORALL = forall(none,[ThisID],TImplication), | |
| 279 | extend_machine_acc(properties,MAcc,FORALL,NewMAcc). | |
| 280 | translate_signature_fact(_TSignatureName,MAcc,Expr,NewMAcc) :- | |
| 281 | translate_e_p(Expr,TExpr) , | |
| 282 | extend_machine_acc(properties,MAcc,TExpr,NewMAcc). | |
| 283 | ||
| 284 | % TO DO: write generic AST traversal predicate | |
| 285 | alloy_expr_contains_join(AndOr) :- | |
| 286 | AndOr =.. [Functor,ListOfAsts,_Pos], !, | |
| 287 | member(Functor,[and,or]), | |
| 288 | member(Ast,ListOfAsts), | |
| 289 | alloy_expr_contains_join(Ast),!. | |
| 290 | alloy_expr_contains_join(identifier('this',_,_)). | |
| 291 | %alloy_expr_contains_join_with_this(join(Arg1,Arg2,_Type,_Pos)) :- | |
| 292 | % Arg1 = identifier('this',_,_) ; Arg2 = identifier('this',_,_). | |
| 293 | alloy_expr_contains_join(Expr) :- | |
| 294 | Expr =.. [_Functor,Arg1,Arg2,_Type,_Pos], !, | |
| 295 | (alloy_expr_contains_join(Arg1) -> true | |
| 296 | ; alloy_expr_contains_join(Arg2)). | |
| 297 | alloy_expr_contains_join(Expr) :- | |
| 298 | Expr =.. [_Functor,Arg,_Type,_Pos] , | |
| 299 | alloy_expr_contains_join(Arg). | |
| 300 | alloy_expr_contains_join(Expr) :- | |
| 301 | Expr =.. [Functor,_Params,Fields,Body,_Type,_POS], | |
| 302 | member(Functor,[all,no,some,one,lone,comprehension]), | |
| 303 | (alloy_expr_contains_join(Body) -> true | |
| 304 | ; member(F,Fields), alloy_expr_contains_join(F) -> true). | |
| 305 | ||
| 306 | % translate fun NAME Decls { Body } or pred Name Decls { Body } | |
| 307 | translate_function(MAcc,FunctionOrPredicate,NewMAcc) :- | |
| 308 | FunctionOrPredicate =.. [Functor,Name,Params,Decls,Body,POS] , | |
| 309 | alloy_to_b_operator(Functor,BFunctor), | |
| 310 | maplist(translate_e_p,Params,TParams), | |
| 311 | % identifier like 'this' are singleton sets, parameters have to be identifiers | |
| 312 | maplist(strip_singleton_set,TParams,TTParams) , | |
| 313 | maplist(translate_function_field,Decls,TDecls), | |
| 314 | translate_e_p(Body,TBody), | |
| 315 | translate_pos(POS,BPOS), | |
| 316 | (Functor == function | |
| 317 | -> (TDecls == [] | |
| 318 | -> TResult = TBody % no need to create set comprehension | |
| 319 | ; % create {temp | TDecls & temp : TBody } | |
| 320 | append(TDecls,[member(none,identifier(none,'_fun_res_'),TBody)],BehaviorList) , | |
| 321 | join_untyped_ast_nodes(conjunct,BehaviorList,Behavior) , | |
| 322 | TResult = comprehension_set(BPOS,[identifier(none,'_fun_res_')],Behavior) | |
| 323 | ), | |
| 324 | UAst =.. [BFunctor,BPOS,Name,TTParams,TResult] | |
| 325 | ; append(TDecls,[TBody],BehaviorList) , | |
| 326 | join_untyped_ast_nodes(conjunct,BehaviorList,Behavior) , | |
| 327 | UAst =.. [BFunctor,BPOS,Name,TTParams,Behavior]) , | |
| 328 | extend_machine_acc(definitions,MAcc,UAst,NewMAcc). | |
| 329 | ||
| 330 | % extract scopes common to all commands | |
| 331 | extract_common_scopes([Cmd|T],GlobalScopes,ExactScopes,UpBoundScopes,BitWidth,MaxSeq,Conflicts) :- | |
| 332 | get_scopes(Cmd,GlobalScopes1,ExactScopes1,UpBound1,BitWidth1,MaxSeq1),!, | |
| 333 | extract_common_aux(T,GlobalScopes1,ExactScopes1,UpBound1,BitWidth1,MaxSeq1,[], | |
| 334 | GlobalScopes,ExactScopes,UpBoundScopes,BitWidth,MaxSeq,Conflicts). | |
| 335 | extract_common_scopes(_,-1,[],[],none,none,[]). | |
| 336 | extract_common_aux([],GS,ES,UpS,BW,MS,C,GS,ES,UpS,BW,MS,C). | |
| 337 | extract_common_aux([Cmd|T],GlobalScope0,ExactScopes0,UpBoundScopes0,BitWidth0,MaxSeq0,Conflicts0, | |
| 338 | GlobalScopes,ExactScopes,UpBoundScopes,BitWidth,MaxSeq,Conflicts) :- | |
| 339 | get_scopes(Cmd,GlobalScope1,ExactScopes1,UpBoundScopes1,BitWidth1,MaxSeq1), | |
| 340 | (GlobalScope0 = GlobalScope1 -> GlobalScope2 = GlobalScope0 ; GlobalScope2=none), | |
| 341 | (BitWidth0 = BitWidth1 -> BitWidth2 = BitWidth1 ; BitWidth2=none), | |
| 342 | (MaxSeq0 = MaxSeq1 -> MaxSeq2 = MaxSeq1 ; MaxSeq2=none), | |
| 343 | join_scopes(ExactScopes0,ExactScopes1,ExactScopes2,Conflicts1), | |
| 344 | ord_union(Conflicts0,Conflicts1,Conflicts2), | |
| 345 | join_scopes(UpBoundScopes0,UpBoundScopes1,UpBoundScopes2,Conflicts3), | |
| 346 | ord_union(Conflicts2,Conflicts3,Conflicts4), | |
| 347 | !, | |
| 348 | extract_common_aux(T,GlobalScope2,ExactScopes2,UpBoundScopes2,BitWidth2,MaxSeq2,Conflicts4, | |
| 349 | GlobalScopes,ExactScopes,UpBoundScopes,BitWidth,MaxSeq,Conflicts). | |
| 350 | ||
| 351 | join_scopes(S1,S2,Inter,Conflicts) :- | |
| 352 | sort(S1,SS1), sort(S2,SS2), ord_intersection(SS1,SS2,Inter), | |
| 353 | ord_union(SS1,SS2,Union), | |
| 354 | ord_subtract(Union,Inter,Conflicts). | |
| 355 | ||
| 356 | get_scopes(Command,GlobalScope,ExactScopes,UpBoundScopes,BitWidth,MaxSeq) :- | |
| 357 | Command =.. [_Functor,_Body,global_scope(GlobalScope), | |
| 358 | exact_scopes(ExactScopes),upper_bound_scopes(UpBoundScopes),BitWidth,MaxSeq|_] , | |
| 359 | !, format('Command scopes: global=~w, exact=~w, upbound=~w,bitwidth=~w~n,maxseq=~w~n', | |
| 360 | [GlobalScope,ExactScopes,UpBoundScopes,BitWidth,MaxSeq]). | |
| 361 | get_scopes(Command,-1,[],[],none,none) :- | |
| 362 | add_error(alloy2b,'Cannot process Alloy Command:',Command). | |
| 363 | ||
| 364 | translate_command(MAcc,Command,NewMAcc) :- | |
| 365 | Command =.. [Functor,Body,GlobalScope,ExactScopes,UpBoundScopes,BitWidth,MaxSeq,index(CommandIndex),POS] , | |
| 366 | % either a model uses no sequences and we translate all commands or only the chosen one | |
| 367 | (\+ uses_seqs ; (current_command(CurrentIndex) , CurrentIndex == CommandIndex)) , ! , | |
| 368 | translate_command_aux(MAcc,Functor,Body,GlobalScope,ExactScopes,UpBoundScopes,BitWidth,MaxSeq,POS,NewMAcc). | |
| 369 | translate_command(MAcc,Command,MAcc) :- | |
| 370 | % only translate the current command if using sequences (either selected by the user or the first one by default) | |
| 371 | Command =.. [_,_,_,_,_,_,_,index(CommandIndex),_] , | |
| 372 | current_command(CurrentIndex) , | |
| 373 | CurrentIndex =\= CommandIndex , !. | |
| 374 | translate_command(MAcc,Command,MAcc) :- | |
| 375 | add_error('Unknown Alloy command (be sure Alloy2B library is up-to-date):',Command). | |
| 376 | ||
| 377 | translate_command_aux(MAcc,Functor,Body,GlobalScope,ExactScopes,UpBoundScopes,BitWidth,MaxSeq,POS,NewMAcc) :- | |
| 378 | debug_println(19,translating_command(Functor,GlobalScope,ExactScopes)), | |
| 379 | (Functor = check ; Functor = run) , | |
| 380 | translate_e_p(Body,TBody) , | |
| 381 | % we need all signature names to define the global scope | |
| 382 | get_signature_names_from_machine_acc(MAcc,SignatureNames) , | |
| 383 | debug_println(19,translate_scopes(SignatureNames)), | |
| 384 | translate_scopes(SignatureNames,GlobalScope,ExactScopes,UpBoundScopes,BitWidth,MaxSeq,TScopesPred) , | |
| 385 | translate_pos(POS,BPOS), | |
| 386 | Precondition = conjunct(BPOS,TScopesPred,TBody) , | |
| 387 | get_command_counter_atom(CommandCounter) , | |
| 388 | atom_concat(Functor,CommandCounter,OperationName) , | |
| 389 | Operation = operation(BPOS,identifier(BPOS,OperationName),[],[],precondition(BPOS,Precondition,skip(none))) , | |
| 390 | extend_machine_acc(operations,MAcc,Operation,NewMAcc) , | |
| 391 | MaxSeq = maxseq(MaxSeqSize) , | |
| 392 | assert(maxseq(MaxSeqSize)). | |
| 393 | ||
| 394 | % global scope, exact scopes and bitwidth | |
| 395 | % We do not need to set the bitwidth since we have real integers in B. | |
| 396 | % Note: If only one command is defined in the Alloy model we could set min and max int of ProB in the definitions. | |
| 397 | translate_scopes(SignatureNames,global_scope(GlobalScope),exact_scopes(ExactScopes),upper_bound_scopes(UpBoundScopes),_BitWidth,maxseq(MaxSeq), | |
| 398 | conjunct(none,SeqScopePred,conjunct(none,TScopes,TGlobalScopes))) :- | |
| 399 | % translate exact and upper bound scopes first | |
| 400 | translate_exact_and_upper_bound_scopes(0,ExactScopes,UpBoundScopes,EUSignatureNames,TScopes,OrdSigCounter1) , | |
| 401 | % if present, define the global scope for the remaining signatures | |
| 402 | translate_global_scope(OrdSigCounter1,GlobalScope,SignatureNames,EUSignatureNames,TGlobalScopes,_) , | |
| 403 | translate_seq_scopes(MaxSeq,SeqScopePred). | |
| 404 | ||
| 405 | translate_seq_scopes(MaxSeq,ScopePred) :- | |
| 406 | findall((Seq,MaxSeq),is_seq(Seq),Seqs) , | |
| 407 | maplist(generate_leq_scope_predicate,Seqs,ScopePreds) , | |
| 408 | join_predicates(conjunct,ScopePreds,ScopePred). | |
| 409 | ||
| 410 | % no exact scopes defined | |
| 411 | translate_exact_and_upper_bound_scopes(OrdSigCounter,[],[],ExactSignatureNames,truth(none),OrdSigCounter) :- !, | |
| 412 | ExactSignatureNames=[]. | |
| 413 | translate_exact_and_upper_bound_scopes(OrdSigCounter,ExactScopes,UpBoundScopes,SignatureNames,TScopes,NewOrdSigCounter) :- | |
| 414 | translate_exact_and_upper_bound_scopes_aux(OrdSigCounter,UpBoundScopes,[], | |
| 415 | UpperBoundSignatureNames,[],TempTUpScopes,OrdSigCounter1) , | |
| 416 | translate_exact_and_upper_bound_scopes_aux(OrdSigCounter1,ExactScopes,[], | |
| 417 | ExactSignatureNames,[],TempTExactScopes,NewOrdSigCounter) , | |
| 418 | append(TempTUpScopes,TempTExactScopes,TempTScopes) , | |
| 419 | append(ExactSignatureNames,UpperBoundSignatureNames,SignatureNames) , | |
| 420 | join_predicates(conjunct,TempTScopes,TScopes). | |
| 421 | ||
| 422 | translate_exact_and_upper_bound_scopes_aux(OrdSigCounter,[],NamesAcc,NamesAcc,TScopeAcc,TScopeAcc,OrdSigCounter). | |
| 423 | translate_exact_and_upper_bound_scopes_aux(OrdSigCounter,[(SignatureName,Scope)|T], | |
| 424 | NameAcc,ExactSignatureNames,TScopeAcc,TempTExactScopes,NewOrdSigCounter) :- | |
| 425 | is_ordered_signature(SignatureName) , ! , | |
| 426 | define_ordered_signature_as_integer_set(OrdSigCounter,SignatureName,Scope, | |
| 427 | TScope,TNewOrdSigCounter) , | |
| 428 | translate_exact_and_upper_bound_scopes_aux(TNewOrdSigCounter,T,[SignatureName|NameAcc], | |
| 429 | ExactSignatureNames,[TScope|TScopeAcc],TempTExactScopes,NewOrdSigCounter). | |
| 430 | translate_exact_and_upper_bound_scopes_aux(OrdSigCounter,[(SignatureName,Scope)|T], | |
| 431 | NameAcc,ExactSignatureNames,TScopeAcc,TempTExactScopes,NewOrdSigCounter) :- | |
| 432 | generate_exact_scope_predicate((SignatureName,Scope),TScope), | |
| 433 | translate_exact_and_upper_bound_scopes_aux(OrdSigCounter,T,[SignatureName|NameAcc], | |
| 434 | ExactSignatureNames,[TScope|TScopeAcc],TempTExactScopes,NewOrdSigCounter). | |
| 435 | ||
| 436 | generate_exact_scope_predicate((SignatureName,Scope),TScopePred) :- | |
| 437 | translate_e_p(SignatureName,TSignatureName), | |
| 438 | %format('Exact scope for SignatureName=~w with scope ~w~n',[SignatureName,Scope]), | |
| 439 | TScopePred = equal(none,card(none,TSignatureName),integer(none,Scope)). | |
| 440 | generate_leq_scope_predicate((SignatureName,Scope),TScopePred) :- | |
| 441 | translate_e_p(SignatureName,TSignatureName) , | |
| 442 | TScopePred = less_equal(none,card(none,TSignatureName),integer(none,Scope)). | |
| 443 | ||
| 444 | define_ordered_signatures_as_integer_set(OrdSigCounter,[],_,[],OrdSigCounter). | |
| 445 | define_ordered_signatures_as_integer_set(OrdSigCounter,[TSignatureName|T],Scope,[TScope|TScopes],NewOrdSigCounter) :- | |
| 446 | define_ordered_signature_as_integer_set(OrdSigCounter,TSignatureName,Scope,TScope,TNewOrdSigCounter) , | |
| 447 | define_ordered_signatures_as_integer_set(TNewOrdSigCounter,T,Scope,TScopes,NewOrdSigCounter). | |
| 448 | ||
| 449 | define_ordered_signature_as_integer_set(OrdSigCounter,TSignatureName,Scope,TScope,NewOrdSigCounter) :- | |
| 450 | NewOrdSigCounter is OrdSigCounter + Scope , | |
| 451 | NewOrdSigCounter1 is NewOrdSigCounter - 1 , | |
| 452 | TScope = equal(none,identifier(none,TSignatureName),interval(none,integer(none,OrdSigCounter),integer(none,NewOrdSigCounter1))). | |
| 453 | ||
| 454 | translate_global_scope(OrdSigCounter,-1,_,_,truth(none),OrdSigCounter) :- !. % no global scope defined | |
| 455 | translate_global_scope(OrdSigCounter,GlobalScope,SignatureNames,ExactSignatureNames,TGlobalScopes,NewOrdSigCounter) :- | |
| 456 | split_ordered_unordered_signatures(SignatureNames,ExactSignatureNames,OrderedSignatureNames,RestSignatureNames) , | |
| 457 | translate_global_scope_aux(RestSignatureNames,GlobalScope,[],TempTGlobalScopes) , | |
| 458 | join_predicates(conjunct,TempTGlobalScopes,TTGlobalScopes) , | |
| 459 | define_ordered_signatures_as_integer_set(OrdSigCounter,OrderedSignatureNames,GlobalScope,TOrderedScopes,NewOrdSigCounter) , | |
| 460 | join_predicates(conjunct,[TTGlobalScopes|TOrderedScopes],TGlobalScopes). | |
| 461 | ||
| 462 | translate_global_scope_aux([],_,Acc,Acc). | |
| 463 | translate_global_scope_aux([SignatureName|T],GlobalScope,Acc,TGlobalScopes) :- | |
| 464 | translate_e_p(SignatureName,TSignatureName) , | |
| 465 | TScope = less_equal(none,card(none,TSignatureName),integer(none,GlobalScope)) , | |
| 466 | translate_global_scope_aux(T,GlobalScope,[TScope|Acc],TGlobalScopes). | |
| 467 | translate_global_scope_aux([_|T],GlobalScope,Acc,TGlobalScopes) :- | |
| 468 | translate_global_scope_aux(T,GlobalScope,Acc,TGlobalScopes). | |
| 469 | ||
| 470 | split_ordered_unordered_signatures(SNames,ExactSNames,OSNames,Rest) :- | |
| 471 | split_ordered_unordered_signatures(SNames,[],[],TOSNames,TRest) , | |
| 472 | % remove exact signatures which are defined separately | |
| 473 | subtract(TOSNames,ExactSNames,OSNames) , | |
| 474 | subtract(TRest,ExactSNames,Rest). | |
| 475 | ||
| 476 | split_ordered_unordered_signatures([],OAcc,RAcc,OAcc,RAcc). | |
| 477 | split_ordered_unordered_signatures([SName|T],OAcc,RAcc,OSNames,Rest) :- | |
| 478 | is_ordered_signature(SName) , | |
| 479 | \+ member(SName,OAcc) , ! , | |
| 480 | split_ordered_unordered_signatures(T,[SName|OAcc],RAcc,OSNames,Rest). | |
| 481 | split_ordered_unordered_signatures([SName|T],OAcc,RAcc,OSNames,Rest) :- | |
| 482 | \+ is_ordered_signature(SName) , | |
| 483 | \+ member(SName,RAcc) , ! , | |
| 484 | split_ordered_unordered_signatures(T,OAcc,[SName|RAcc],OSNames,Rest). | |
| 485 | split_ordered_unordered_signatures([_|T],OAcc,RAcc,OSNames,Rest) :- | |
| 486 | split_ordered_unordered_signatures(T,OAcc,RAcc,OSNames,Rest). | |
| 487 | ||
| 488 | % signature in (subset) | |
| 489 | define_sig_as_set_or_constant(MAcc,Name,Options,POS,NewMAcc) :- | |
| 490 | memberchk(subset(Parents),Options) , ! , | |
| 491 | % maplist(assert_extending_signature(Name),Parents) , % subset signatures do not need to be distinct | |
| 492 | translate_pos(POS,BPOS), | |
| 493 | define_sig_as_set_or_constant_aux(constants,MAcc,Name,Options,BPOS,MAcc1) , | |
| 494 | % TODO: consider several parents -> we need the universe type | |
| 495 | Parents = [Parent|_], | |
| 496 | translate_e_p(Name,TName), | |
| 497 | translate_e_p(Parent,TParent), | |
| 498 | TNode = subset(BPOS,TName,TParent) , | |
| 499 | extend_machine_acc(properties,MAcc1,TNode,NewMAcc). | |
| 500 | % signature extends | |
| 501 | define_sig_as_set_or_constant(MAcc,Name,Options,POS,NewMAcc) :- | |
| 502 | member(subsig(Parent),Options), | |
| 503 | !, | |
| 504 | (member(one,Options) -> One=one ; One=set), | |
| 505 | assert_extending_signature(Name,Parent,One), | |
| 506 | translate_pos(POS,BPOS), | |
| 507 | define_sig_as_set_or_constant_aux(constants,MAcc,Name,Options,BPOS,MAcc1), | |
| 508 | translate_e_p(Name,TName), | |
| 509 | translate_e_p(Parent,TParent), | |
| 510 | TNode = subset(BPOS,TName,TParent), | |
| 511 | extend_machine_acc(properties,MAcc1,TNode,NewMAcc). | |
| 512 | % default signature | |
| 513 | define_sig_as_set_or_constant(MAcc,Name,Options,POS,NewMAcc) :- | |
| 514 | translate_pos(POS,BPOS), | |
| 515 | define_sig_as_set_or_constant_aux(sets,MAcc,Name,Options,BPOS,NewMAcc). | |
| 516 | ||
| 517 | define_sig_as_set_or_constant_aux(sets,MAcc,Name,Options,BPOS,NewMAcc) :- | |
| 518 | member(one,Options) , ! , | |
| 519 | atom_concat('_',Name,EnumElement) , | |
| 520 | % TODO: couldn't figure out untyped ast of enumerated set, define enumerated set S = {_S} instead of constant etc. | |
| 521 | extend_machine_acc(sets,MAcc,deferred_set(BPOS,Name),MAcc1) , | |
| 522 | extend_machine_acc(constants,MAcc1,identifier(BPOS,EnumElement),MAcc2) , | |
| 523 | extend_machine_acc(properties,MAcc2,equal(BPOS,identifier(BPOS,Name),set_extension(BPOS,[identifier(BPOS,EnumElement)])),NewMAcc). | |
| 524 | define_sig_as_set_or_constant_aux(sets,MAcc,Name,Options,BPOS,NewMAcc) :- | |
| 525 | member(some,Options) , ! , | |
| 526 | extend_machine_acc(sets,MAcc,deferred_set(BPOS,Name),MAcc1) , | |
| 527 | extend_machine_acc(properties,MAcc1,greater_equal(BPOS,card(BPOS,identifier(BPOS,Name)),integer(BPOS,1)),NewMAcc). | |
| 528 | define_sig_as_set_or_constant_aux(sets,MAcc,Name,Options,BPOS,NewMAcc) :- | |
| 529 | member(lone,Options) , ! , | |
| 530 | extend_machine_acc(sets,MAcc,deferred_set(BPOS,Name),MAcc1) , | |
| 531 | extend_machine_acc(properties,MAcc1,less_equal(BPOS,card(BPOS,identifier(BPOS,Name)),integer(BPOS,1)),NewMAcc). | |
| 532 | define_sig_as_set_or_constant_aux(sets,MAcc,Name,_Options,BPOS,NewMAcc) :- | |
| 533 | extend_machine_acc(sets,MAcc,deferred_set(BPOS,Name),NewMAcc). | |
| 534 | define_sig_as_set_or_constant_aux(constants,MAcc,Name,_Options,BPOS,NewMAcc) :- | |
| 535 | extend_machine_acc(constants,MAcc,identifier(BPOS,Name),NewMAcc). | |
| 536 | ||
| 537 | % -------- | |
| 538 | % Semantic translation rules: translate expression or predicate | |
| 539 | % -------- | |
| 540 | ||
| 541 | translate_e_p(A,TA) :- %% functor(A,F,N),format('~n TRANSLATE: ~w/~w : ~w ~n',[F,N,A]), | |
| 542 | translate_quantifier_e(A,TA) , !. | |
| 543 | translate_e_p(A,TA) :- | |
| 544 | translate_cst_e_p(A,TA) , !. | |
| 545 | translate_e_p(A,TA) :- | |
| 546 | translate_unary_e_p(A,TA) , !. | |
| 547 | translate_e_p(A,TA) :- | |
| 548 | translate_binary_e_p(A,TA) , !. | |
| 549 | translate_e_p(A,TA) :- | |
| 550 | translate_if_then_else(A,TA). | |
| 551 | translate_e_p(A,_) :- | |
| 552 | add_error(load_alloy_model,'Translation failed for:',A),fail. | |
| 553 | ||
| 554 | % Translation in the context where we expect an integer | |
| 555 | translate_e_p_integer(integer(A,POS),integer(BPOS,A)) :- !, | |
| 556 | translate_pos(POS,BPOS). | |
| 557 | translate_e_p_integer(identifier(ID,_Type,POS),identifier(BPOS,ID)) :- % translate without the set_extension | |
| 558 | is_singleton_set_id(ID) , !, | |
| 559 | translate_pos(POS,BPOS). | |
| 560 | translate_e_p_integer(A,TA) :- | |
| 561 | translate_e_p(A,TSetA), | |
| 562 | (TSetA = set_extension(_,[Single]) | |
| 563 | -> TA = Single | |
| 564 | ; get_position(A,BPOS), | |
| 565 | add_message(translate_e_p_integer,'Notice: using MU operator, could not statically extract integer singleton set for: ',TSetA,BPOS), | |
| 566 | %construct_choose(TSetA,TA) | |
| 567 | TA = mu(BPOS,TSetA) % use the Zed MU operator | |
| 568 | ). | |
| 569 | ||
| 570 | %construct_choose(TSetA,external_function_call(none,'CHOOSE',[TSetA],string(none,'a member of X'),TypeParams,Decl)) :- | |
| 571 | % % format of raw AST of CHOOSE copied from btype2 | |
| 572 | % TypeParams = rewrite_protected([identifier(none,T)]), | |
| 573 | % Decl = rewrite_protected(total_function(none,pow_subset(none,identifier(none,T)),identifier(none,T))). | |
| 574 | ||
| 575 | translate_if_then_else(if_then_else(ConditionPred,TruthExpr,FalsityExpr,_Type,POS),TIfThenElse) :- | |
| 576 | translate_e_p(ConditionPred,TConditionPred), | |
| 577 | translate_e_p(TruthExpr,TTruthExpr), | |
| 578 | translate_e_p(FalsityExpr,TFalsityExpr), | |
| 579 | translate_pos(POS,BPOS), | |
| 580 | get_type_and_arity_from_alloy_term(TruthExpr,Type,_), | |
| 581 | ((Type = [untyped] ; is_primitive_type(Type,_)) | |
| 582 | -> TIfThenElse = conjunct(BPOS, | |
| 583 | implication(BPOS,TConditionPred,TTruthExpr), | |
| 584 | implication(BPOS,negation(BPOS,TConditionPred),TFalsityExpr)) | |
| 585 | ; TIfThenElse = if_then_else(BPOS,TConditionPred,TTruthExpr,TFalsityExpr) | |
| 586 | ). | |
| 587 | ||
| 588 | translate_quantifier_e(Quantifier,TQuantifier) :- | |
| 589 | Quantifier =.. [Functor,Params,Fields,Body,_Type,POS], | |
| 590 | member(Functor,[all,no,some,one,lone,comprehension]), | |
| 591 | maplist(translate_e_p,Params,TParams), | |
| 592 | maplist(strip_singleton_set,TParams,TTParams) , % more of a hack; we should ensure singleton_set is properly set | |
| 593 | translate_pos(POS,BPOS), | |
| 594 | maplist(translate_quantifier_field,Fields,TFieldsList,SingletonSetNames), | |
| 595 | (is_disjoint_quantifier(Fields) | |
| 596 | -> maplist(translate_e_p,SingletonSetNames,TSets), | |
| 597 | AllDiff = equal(BPOS,card(BPOS,general_union(BPOS,set_extension(BPOS,TSets))),integer(BPOS,Len)), | |
| 598 | length(Fields,Len), | |
| 599 | %print(disjoint(Len)),nl, | |
| 600 | join_untyped_ast_nodes(conjunct,[AllDiff|TFieldsList],TFields) | |
| 601 | ; join_untyped_ast_nodes(conjunct,TFieldsList,TFields) | |
| 602 | ), | |
| 603 | translate_e_p(Body,TBody), | |
| 604 | translate_quantifier_e_aux(BPOS,Functor,TTParams,TFields,TBody,TQuantifier), | |
| 605 | maplist(retract_singleton_set(BPOS),Params), | |
| 606 | maplist(retract_singleton_set(BPOS),SingletonSetNames). | |
| 607 | ||
| 608 | translate_quantifier_e_aux(Pos,all,TParams,TFields,TBody,forall(Pos,TParams,implication(none,TFields,TBody))). | |
| 609 | translate_quantifier_e_aux(Pos,no,TParams,TFields,TBody,negation(Pos,exists(none,TParams,conjunct(none,TFields,TBody)))). | |
| 610 | translate_quantifier_e_aux(Pos,some,TParams,TFields,TBody,exists(Pos,TParams,conjunct(none,TFields,TBody))). | |
| 611 | translate_quantifier_e_aux(Pos,one,TParams,TFields,TBody,equal(Pos,card(none,comprehension_set(none,TParams,conjunct(none,TFields,TBody))),integer(none,1))). | |
| 612 | translate_quantifier_e_aux(Pos,lone,TParams,TFields,TBody,less_equal(Pos,card(none,comprehension_set(none,TParams,conjunct(none,TFields,TBody))),integer(none,1))). | |
| 613 | translate_quantifier_e_aux(Pos,comprehension,TParams,TFields,TBody,comprehension_set(Pos,TParams,conjunct(none,TFields,TBody))). | |
| 614 | ||
| 615 | % Translate Constants | |
| 616 | translate_cst_e_p(iden(POS),event_b_identity(BPOS)) :- % has no Span Info ! | |
| 617 | translate_pos(POS,BPOS). | |
| 618 | translate_cst_e_p(identifier(Cst,_,POS),BConstruct) :- | |
| 619 | alloy_constant_to_b(Cst,BPOS,BConstruct),!, | |
| 620 | translate_pos(POS,BPOS). | |
| 621 | translate_cst_e_p(this,_) :- print('this not yet translated'),nl,fail. | |
| 622 | ||
| 623 | ||
| 624 | alloy_constant_to_b(none,BPOS,empty_set(BPOS)). | |
| 625 | alloy_constant_to_b('boolean''False',BPOS,boolean_false(BPOS)). | |
| 626 | alloy_constant_to_b('boolean''True',BPOS,boolean_true(BPOS)). | |
| 627 | ||
| 628 | ||
| 629 | translate_unary_e_p(string(StringCodes,POS),set_extension(BPOS,[string(BPOS,String)])) :- | |
| 630 | atom_codes(String,StringCodes) , ! , | |
| 631 | translate_pos(POS,BPOS). | |
| 632 | translate_unary_e_p(seq(ID),sequence_extension(none,TID)) :- | |
| 633 | translate_unary_e_p(ID,TID) , !. | |
| 634 | translate_unary_e_p(Int,integer(none,Int)) :- integer(Int) , !. | |
| 635 | translate_unary_e_p(identifier(ID,_Type,POS),set_extension(BPOS,[identifier(BPOS,NID)])) :- | |
| 636 | % singleton enumerated set like S = {_S} | |
| 637 | enumerated_set(ID) , | |
| 638 | is_singleton_set_id(ID) , !, | |
| 639 | atom_concat('_',ID,NID) , | |
| 640 | translate_pos(POS,BPOS). | |
| 641 | translate_unary_e_p(identifier(ID,_Type,POS),set_extension(BPOS,[identifier(BPOS,ID)])) :- | |
| 642 | is_singleton_set_id(ID) , !, | |
| 643 | translate_pos(POS,BPOS). | |
| 644 | translate_unary_e_p(ID,set_extension(none,[identifier(none,NID)])) :- | |
| 645 | enumerated_set(ID) , | |
| 646 | is_singleton_set_id(ID) , ! , | |
| 647 | atom_concat('_',ID,NID). | |
| 648 | translate_unary_e_p(ID,set_extension(none,[identifier(none,ID)])) :- | |
| 649 | is_singleton_set_id(ID) , !. % DOES THIS EVER TRIGGER ? | |
| 650 | translate_unary_e_p(integer(A,POS),set_extension(BPOS,[integer(BPOS,A)])) :- !, | |
| 651 | translate_pos(POS,BPOS). | |
| 652 | translate_unary_e_p(identifier('Int',_Type,POS),integer_set(BPOS,'INTEGER')) :- !, | |
| 653 | translate_pos(POS,BPOS). | |
| 654 | translate_unary_e_p(identifier('String',_,_),string_set(none)) :- !. | |
| 655 | translate_unary_e_p('Int',integer_set(none,'INTEGER')) :- !. | |
| 656 | translate_unary_e_p(identifier(ID,_Type,POS),identifier(BPOS,ID)) :- !,translate_pos(POS,BPOS). | |
| 657 | translate_unary_e_p(boolean(true,POS),truth(BPOS)) :- !, % was boolean_true, but Alloy has no booleans | |
| 658 | translate_pos(POS,BPOS). | |
| 659 | translate_unary_e_p(boolean(false,POS),falsity(BPOS)) :- !, % was boolean_false | |
| 660 | translate_pos(POS,BPOS). | |
| 661 | translate_unary_e_p(Type,integer_set(none,'INTEGER')) :- | |
| 662 | % lhs of sequence is integer, Alloy Types are like [seqInt,A] for set(couple(INTEGER,A)) | |
| 663 | atom(Type) , atom_concat(seq,_,Type) , !. | |
| 664 | translate_unary_e_p(ID,identifier(none,ID)) :- atom(ID) , !. | |
| 665 | translate_unary_e_p(UnaryP,TUnaryP) :- | |
| 666 | % and/or defines a list of ast nodes | |
| 667 | UnaryP =.. [Op,ArgList|_] , | |
| 668 | memberchk(Op,[and,or]) , % translated to conjunct/disjunct | |
| 669 | is_list(ArgList) , ! , | |
| 670 | maplist(translate_e_p,ArgList,TArgList) , | |
| 671 | join_predicates(Op,TArgList,TUnaryP). | |
| 672 | translate_unary_e_p(UnaryP,TUnaryP) :- | |
| 673 | UnaryP =.. [Op,Arg,_Type,POS] , | |
| 674 | member(Op,[no,one,some,lone]) , ! , | |
| 675 | translate_e_p(Arg,TArg), | |
| 676 | translate_pos(POS,BPOS), | |
| 677 | translate_quantified_e(BPOS,Op,TArg,TUnaryP). | |
| 678 | translate_unary_e_p(card(Arg,_Type,POS),set_extension(BPOS,[card(BPOS,TArg)])) :- !, % wrap card into set extension | |
| 679 | translate_e_p(Arg,TArg), | |
| 680 | translate_pos(POS,BPOS). | |
| 681 | translate_unary_e_p(UnaryP,TUnaryP) :- | |
| 682 | UnaryP =.. [Op,Arg,_Type,POS] , | |
| 683 | translate_e_p(Arg,TArg) , | |
| 684 | alloy_to_b_unary_operator(Op,BOp), | |
| 685 | translate_pos(POS,BPOS), | |
| 686 | TUnaryP =.. [BOp,BPOS,TArg]. | |
| 687 | ||
| 688 | ||
| 689 | % FUNCTIONS defined by func in util: | |
| 690 | ||
| 691 | %alloy_utility_function(Name,Arity,BOperator,ArgType,ReturnType). | |
| 692 | alloy_utility_function(Name,Arity,BOperator,integer,integer) :- | |
| 693 | alloy_to_b_integer_to_integer_func(Name,Arity,BOperator). | |
| 694 | alloy_utility_function(Name,Arity,BOperator,set,integer) :- | |
| 695 | alloy_to_b_integer_func(Name,Arity,BOperator). | |
| 696 | alloy_utility_function(Name,Arity,BOperator,integer,set) :- | |
| 697 | alloy_to_b_integer_operator_func(Name,Arity,BOperator). | |
| 698 | alloy_utility_function(Name,Arity,BOperator,set,set) :- | |
| 699 | alloy_to_b_operator_func(Name,Arity,BOperator). | |
| 700 | ||
| 701 | % functions with integer arguments and result | |
| 702 | alloy_to_b_integer_to_integer_func('integer''minus',2,minus). | |
| 703 | alloy_to_b_integer_to_integer_func('integer''plus',2,add). | |
| 704 | alloy_to_b_integer_to_integer_func('integer''div',2,div). | |
| 705 | alloy_to_b_integer_to_integer_func('integer''mul',2,multiplication). | |
| 706 | alloy_to_b_integer_to_integer_func('integer''rem',2,modulo). | |
| 707 | %alloy_to_b_integer_to_integer_func('integer''sum',sigma). % TO DO: translate sum | |
| 708 | alloy_to_b_integer_to_integer_func('integer''add',2,add). | |
| 709 | alloy_to_b_integer_to_integer_func('integer''sub',2,minus). | |
| 710 | %alloy_to_b_integer_to_integer_func('integer''smaller',max). % TO DO: if Arg1 < Arg2 then Arg1 else Arg2 end | |
| 711 | ||
| 712 | % Unary: | |
| 713 | alloy_to_b_integer_to_integer_func('integer''negate',1,unary_minus). | |
| 714 | alloy_to_b_integer_to_integer_func('integer''next',1,successor). % not sure this is called; seems to call arity 0 and use join | |
| 715 | alloy_to_b_integer_to_integer_func('integer''prev',1,predecessor). | |
| 716 | ||
| 717 | ||
| 718 | % functions with integer result but set arguments | |
| 719 | alloy_to_b_integer_func('integer''min',1,min). | |
| 720 | alloy_to_b_integer_func('integer''max',1,max). | |
| 721 | alloy_to_b_integer_func('integer''min',0,min_int). % TO DO: investigate bit-width related translation | |
| 722 | alloy_to_b_integer_func('integer''max',0,max_int). % maybe we should have a preference for Alloy2B about INT/INTEGER | |
| 723 | % Note: for run Arithmetic for 6 Int the Alloy Evaluator produces {-32} for min and {+31} for max | |
| 724 | ||
| 725 | % predicate functions with integer arguments | |
| 726 | alloy_to_b_operator_func('integer''next',0,successor). | |
| 727 | alloy_to_b_operator_func('integer''prev',0,predecessor). | |
| 728 | ||
| 729 | % predicate functions with integer arguments | |
| 730 | alloy_to_b_integer_operator_func('integer''gt',2,greater). | |
| 731 | alloy_to_b_integer_operator_func('integer''lt',2,less). | |
| 732 | alloy_to_b_integer_operator_func('integer''gte',2,greater_equal). | |
| 733 | alloy_to_b_integer_operator_func('integer''lte',2,less_equal). | |
| 734 | alloy_to_b_integer_operator_func('integer''eq',2,equal). | |
| 735 | ||
| 736 | % dom[r] = dom(r) | |
| 737 | alloy_to_b_relational_utility_function('relation''dom',[Param],_Type,BPOS,TCall) :- ! , | |
| 738 | translate_e_p(Param,TParam) , | |
| 739 | TCall = dom(BPOS,TParam). | |
| 740 | % ran[r] = ran(r) | |
| 741 | alloy_to_b_relational_utility_function('relation''ran',[Param],_Type,BPOS,TCall) :- ! , | |
| 742 | translate_e_p(Param,TParam) , | |
| 743 | TCall = range(BPOS,TParam). | |
| 744 | % total[r,d] = !x.(x:d => r[{x}] /= {}}) | |
| 745 | alloy_to_b_relational_utility_function('relation''total',[Relation,Domain],_Type,BPOS,TCall) :- ! , | |
| 746 | translate_e_p(Relation,TRelation) , | |
| 747 | translate_e_p(Domain,TDomain) , | |
| 748 | gen_identifier(0,"_c_",ID0), | |
| 749 | LHS = member(BPOS,ID0,TDomain) , | |
| 750 | RHS = not_equal(BPOS,image(BPOS,TRelation,set_extension(BPOS,[ID0])),empty_set(BPOS)) , | |
| 751 | TCall = forall(BPOS,[ID0],implication(BPOS,LHS,RHS)). | |
| 752 | % functional[r,d] = !x.(x:d => card(r[{x}]) <= 1) | |
| 753 | alloy_to_b_relational_utility_function('relation''functional',[Relation,Domain],_Type,BPOS,TCall) :- ! , | |
| 754 | translate_e_p(Relation,TRelation) , | |
| 755 | translate_e_p(Domain,TDomain) , | |
| 756 | gen_identifier(0,"_c_",ID0), | |
| 757 | LHS = member(BPOS,ID0,TDomain) , | |
| 758 | RHS = less_equal(BPOS,card(BPOS,image(BPOS,TRelation,set_extension(BPOS,[ID0]))),integer(BPOS,1)) , | |
| 759 | TCall = forall(BPOS,[ID0],implication(BPOS,LHS,RHS)). | |
| 760 | % function[r,d] = !x.(x:d => card(r[{x}]) = 1) | |
| 761 | alloy_to_b_relational_utility_function('relation''function',[Relation,Domain],_Type,BPOS,TCall) :- ! , | |
| 762 | translate_e_p(Relation,TRelation) , | |
| 763 | translate_e_p(Domain,TDomain) , | |
| 764 | gen_identifier(0,"_c_",ID0), | |
| 765 | LHS = member(BPOS,ID0,TDomain) , | |
| 766 | RHS = equal(BPOS,card(BPOS,image(BPOS,TRelation,set_extension(BPOS,[ID0]))),integer(BPOS,1)) , | |
| 767 | TCall = forall(BPOS,[ID0],implication(BPOS,LHS,RHS)). | |
| 768 | % injective[r,d] = !(x).(x:d => card(r~[{x}]) <= 1) | |
| 769 | alloy_to_b_relational_utility_function('relation''injective',[Relation,Domain],_Type,BPOS,TCall) :- ! , | |
| 770 | translate_e_p(Relation,TRelation) , | |
| 771 | translate_e_p(Domain,TDomain) , | |
| 772 | gen_identifier(0,"_c_",ID0), | |
| 773 | LHS = member(BPOS,ID0,TDomain) , | |
| 774 | RHS = less_equal(BPOS,card(BPOS,image(BPOS,reverse(BPOS,TRelation),set_extension(BPOS,[ID0]))),integer(BPOS,1)) , | |
| 775 | TCall = forall(BPOS,[ID0],implication(BPOS,LHS,RHS)). | |
| 776 | alloy_to_b_relational_utility_function(FunName,_,_,BPOS,truth(BPOS)) :- | |
| 777 | atom_concat('relation',_,FunName) , ! , | |
| 778 | add_error(alloy_to_b_relational_utility_function,'Function from util/relation currently not supported',[],BPOS). | |
| 779 | % TODO: implement rest as described in the article | |
| 780 | ||
| 781 | %remove_prime(Old,New) :- atom_codes(Old,OldC) , delete(OldC,39,NewC) , atom_codes(New,NewC). | |
| 782 | ||
| 783 | get_clean_ordering_fun_name(OrderingFunctionName,CleanOrdFunName) :- | |
| 784 | member(CleanOrdFunName,[first,last,min,max,next,nexts,prev,prevs,larger,smaller,lt,lte,gt,gte]) , | |
| 785 | atom_concat(_,CleanOrdFunName,OrderingFunctionName). | |
| 786 | ||
| 787 | get_ordering_definition_name(TempFunctionName,SignatureName,FunctionName) :- | |
| 788 | member(TempFunctionName,[next,prev,nexts,prevs]) , | |
| 789 | atom_concat(TempFunctionName,'_',TTempFunctionName) , | |
| 790 | atom_concat(TTempFunctionName,SignatureName,FunctionName). | |
| 791 | ||
| 792 | translate_binary_e_p(in(Arg1,Arg2,_Type,POS),Translation) :- !, | |
| 793 | translate_pos(POS,BPOS), translate_e_p(Arg1,TArg1), | |
| 794 | translate_binary_in(TArg1,Arg2,BPOS,Translation). | |
| 795 | translate_binary_e_p(CartTerm,TCartesian) :- | |
| 796 | is_cartesian_product_term(CartTerm,Arg1,Arg2,POS), | |
| 797 | !, | |
| 798 | translate_pos(POS,BPOS), | |
| 799 | translate_cartesian(BPOS,Arg1,Arg2,TCartesian). | |
| 800 | % S <: Rel --> {x1,..,xk| x1:S & (x1,...,xk):Rel} | |
| 801 | translate_binary_e_p(dom_restr(Arg1,Arg2,_Type,POS),TDom) :- | |
| 802 | \+ is_binary_relation(Arg2), % for binary relation translation to B domain_restriction works | |
| 803 | !, | |
| 804 | get_type_and_arity_from_alloy_term(Arg2,_,Arity), | |
| 805 | gen_ids_and_couple(Arity,IDS,Couple), | |
| 806 | translate_pos(POS,BPOS), | |
| 807 | TDom = comprehension_set(BPOS,IDS,conjunct(BPOS,Mem1,Mem2)), | |
| 808 | IDS = [ID1|_], | |
| 809 | Mem1 = member(TPos,ID1,TArg1), | |
| 810 | Mem2 = member(TPos,Couple,TArg2), | |
| 811 | translate_e_p(Arg1,TArg1), | |
| 812 | translate_e_p(Arg2,TArg2). | |
| 813 | translate_binary_e_p(join(Arg1,Arg2,_Type,POS),TJoin) :- !, | |
| 814 | translate_pos(POS,BPOS), | |
| 815 | translate_join(BPOS,Arg1,Arg2,TJoin). | |
| 816 | translate_binary_e_p(let(VarName,Expr,Sub,Type,POS),TLet) :- ! , | |
| 817 | translate_e_p(VarName,TVarName) , | |
| 818 | translate_e_p(Expr,TExpr) , | |
| 819 | (Type == type(['PrimitiveBoolean'],0) -> NewFunctor = let_predicate ; NewFunctor = let_expression) , | |
| 820 | translate_e_p(Sub,TSub) , | |
| 821 | translate_pos(POS,BPOS) , | |
| 822 | TLet =.. [NewFunctor,BPOS,[TVarName],equal(BPOS,TVarName,TExpr),TSub]. | |
| 823 | translate_binary_e_p(Call,TCall) :- | |
| 824 | Call =.. [Functor,Name,Params,Type,POS] , | |
| 825 | (Functor = pred_call ; Functor = fun_call ) , ! , | |
| 826 | translate_pos(POS,BPOS), | |
| 827 | translate_function_call(Name,Params,Type,BPOS,TCall). | |
| 828 | translate_binary_e_p(Binary,TBinary) :- | |
| 829 | Binary =.. [Op,Arg1,Arg2,_Type,POS] , | |
| 830 | alloy_to_b_integer_operator(Op,BOp), !, | |
| 831 | translate_e_p_integer(Arg1,TArg1), | |
| 832 | translate_e_p_integer(Arg2,TArg2), | |
| 833 | translate_pos(POS,BPOS), | |
| 834 | TBinary =.. [BOp,BPOS,TArg1,TArg2]. | |
| 835 | translate_binary_e_p(Binary,TBinary) :- | |
| 836 | Binary =.. [Op,Arg1,Arg2,_Type,POS] , | |
| 837 | alloy_to_b_binary_operator(Op,BOp), | |
| 838 | translate_e_p(Arg1,TArg1), | |
| 839 | translate_e_p(Arg2,TArg2), | |
| 840 | translate_pos(POS,BPOS), | |
| 841 | TBinary =.. [BOp,BPOS,TArg1,TArg2]. | |
| 842 | ||
| 843 | % translate TArg1 in Arg2 (multplicity are not allowed for not in) | |
| 844 | translate_binary_in(TArg1,Arg2,BPOS,Translation) :- | |
| 845 | compound(Arg2),functor(Arg2,Functor,4), % binary operator, | |
| 846 | alloy_to_b_special_multiplicity_type(Functor,_,_,_,_), | |
| 847 | !, | |
| 848 | Translation = member(BPOS,TArg1,TArg2), % use element of rather than subset for special type opererators | |
| 849 | translate_special_multiplicity_binary_e_p(Arg2,TArg2). | |
| 850 | translate_binary_in(TArg1,Arg2,BPOS,subset(BPOS,TArg1,TArg2)) :- | |
| 851 | translate_e_p(Arg2,TArg2). | |
| 852 | ||
| 853 | /* | |
| 854 | not yet finished: | |
| 855 | % replace Arg1 M -> N Arg2 to pure cartesian product and generate predicates | |
| 856 | translate_multiplicity_to_cartesian_and_pred(cartesian(A,B,Type,Pos),LHS,Left,Right,Res) :- !, | |
| 857 | Res = cartesian(CA,CB,Type,Pos), | |
| 858 | get_type_and_arity_from_alloy_term(CA,_Type,ArityA), L2 is Left+ArityA, | |
| 859 | get_type_and_arity_from_alloy_term(CB,_Type,ArityB), R1 is Right-ArityB, | |
| 860 | translate_multiplicity_to_cartesian_and_pred(A,LHS,Left,R1,CA), | |
| 861 | translate_multiplicity_to_cartesian_and_pred(B,LHS,L2,Right,CB). | |
| 862 | translate_multiplicity_to_cartesian_and_pred(Binary,LHS,Left,Right,Res) :- | |
| 863 | Binary =.. [Op,Arg1,Arg2,Type,POS] , | |
| 864 | alloy_to_b_special_multiplicity_type(Op,BOp,LHSMult,RHSMult,ok), | |
| 865 | !, | |
| 866 | % TO DO: add extra predicates | |
| 867 | create_dom(Left,LHS,Pos,Proj1), % project away leftmost tuples | |
| 868 | create_ran(Right,Proj1,Pos,Proj2), % project away rightmost tuples | |
| 869 | ||
| 870 | translate_multiplicity_to_cartesian_and_pred(cartesian(A,B,Type,Pos),LHS,Left,Right,Res). | |
| 871 | translate_multiplicity_to_cartesian_and_pred(A,_,_,_,A). | |
| 872 | ||
| 873 | % create_dom(N,Expr,Pos,Res): create dom(...(dom(Expr))) to project away the leftmost N Arguments of Expr | |
| 874 | create_dom(0,E,_,Res) :- !, Res=E. | |
| 875 | create_dom(N,E,Pos,domain(Pos,D1)) :- N>0, N1 is N-1, | |
| 876 | create_dom(N1,E,Pos,D1). | |
| 877 | ||
| 878 | create_ran(0,E,_,Res) :- !, Res=E. | |
| 879 | */ | |
| 880 | ||
| 881 | % translate expressions of the form Arg1 MULT -> MULT Arg2 with MULT : {some,lone, one, ''} | |
| 882 | % The result is to be used in member(Pos,LHS,TBinary) not for subset checks ! | |
| 883 | translate_special_multiplicity_binary_e_p(Binary,TBinary) :- | |
| 884 | Binary =.. [Op,Arg1,Arg2,_Type,POS] , | |
| 885 | alloy_to_b_special_multiplicity_type(Op,BOp,_,_,ok), | |
| 886 | translate_e_p(Arg1,TArg1), | |
| 887 | translate_e_p(Arg2,TArg2), | |
| 888 | translate_pos(POS,BPOS), | |
| 889 | TBinary =.. [BOp,BPOS,TArg1,TArg2]. | |
| 890 | ||
| 891 | % TODO: update sequence implementation as described in the article | |
| 892 | ||
| 893 | % Note: Sequences in B are indexed from 1 to n, in Alloy from 0 to n-1. | |
| 894 | % Documentation available at http://alloy.lcs.mit.edu/alloy/documentation/quickguide/seq.html | |
| 895 | % Sequence function calls without a parameter but the sequence itself. | |
| 896 | % butlast: seq[{size(seq)-1}] | |
| 897 | sequence_function_to_b('seq\'butlast',BPOS,[Seq],image(BPOS,Seq,set_extension(BPOS,[minus(BPOS,size(BPOS,Seq),integer(BPOS,1))]))). | |
| 898 | % isEmpty: seq = <> | |
| 899 | sequence_function_to_b('seq\'isEmpty',BPOS,[Seq],equal(BPOS,Seq,empty_sequence(BPOS))). | |
| 900 | % hasDups: size(seq) /= card(ran(seq)) | |
| 901 | sequence_function_to_b('seq\'hasDups',BPOS,[Seq],not_equal(BPOS,size(BPOS,Seq),card(BPOS,range(BPOS,Seq)))). | |
| 902 | % inds: {x|x:1..size(seq)} | |
| 903 | sequence_function_to_b('seq\'inds',BPOS,[Seq],comprehension_set(BPOS,[identifier(BPOS,x)],member(BPOS,identifier(BPOS,x),interval(BPOS,integer(BPOS,1),size(BPOS,Seq))))). | |
| 904 | % lastIdx: LET x BE x = size(seq) IN (IF x > 0 THEN {x} ELSE {} END) END | |
| 905 | % TO DO: use let like let_expression(BPOS,[identifier(BPOS,x)],equal(BPOS,identifier(BPOS,x),size(BPOS,Seq)),if_then_else(BPOS,greater(BPOS,identifier(BPOS,x),integer(BPOS,0)),set_extension(BPOS,[identifier(BPOS,x)]),empty_set(BPOS))) | |
| 906 | sequence_function_to_b('seq\'lastIdx',BPOS,[Seq],let_expression(BPOS,[identifier(BPOS,x)],equal(BPOS,identifier(BPOS,x),size(BPOS,Seq)),if_then_else(BPOS,greater(BPOS,identifier(BPOS,x),integer(BPOS,0)),set_extension(BPOS,[identifier(BPOS,x)]),empty_set(BPOS)))). | |
| 907 | % afterLastIdx: LET x BE x = size(seq) IN (IF x < MAXSEQ THEN {x} ELSE {} END) END | |
| 908 | % TO DO: use let like let_expression(BPOS,[identifier(BPOS,x)],equal(BPOS,identifier(BPOS,x),size(BPOS,Seq)),if_then_else(BPOS,less(BPOS,identifier(BPOS,x),integer(BPOS,MaxSeq)),set_extension(BPOS,[identifier(BPOS,x)]),empty_set(BPOS))) | |
| 909 | sequence_function_to_b('seq\'afterLastIdx',BPOS,[Seq],let_expression(BPOS,[identifier(BPOS,x)],equal(BPOS,identifier(BPOS,x),size(BPOS,Seq)),if_then_else(BPOS,less(BPOS,identifier(BPOS,x),integer(BPOS,MaxSeq)),set_extension(BPOS,[identifier(BPOS,x)]),empty_set(BPOS)))) :- | |
| 910 | maxseq(MaxSeq). | |
| 911 | % Sequence function calls with one parameter and the sequence itself. | |
| 912 | % idxOf[elm]: IF size(seq) > 0 THEN {min(seq~[{elm}])} ELSE {} END | |
| 913 | sequence_function_to_b('seq\'idxOf',BPOS,[Seq,P1],if_then_else(BPOS,not_equal(BPOS,image(BPOS,reverse(BPOS,Seq),P1),empty_set(BPOS)),set_extension(BPOS,[min(BPOS,image(BPOS,reverse(BPOS,Seq),P1))]),empty_set(BPOS))). | |
| 914 | % lastIdxOf[elm]: IF size(seq) > 0 THEN {max(seq~[{elm}])} ELSE {} END | |
| 915 | sequence_function_to_b('seq\'lastIdxOf',BPOS,[Seq,P1],if_then_else(BPOS,not_equal(BPOS,image(BPOS,reverse(BPOS,Seq),P1),empty_set(BPOS)),set_extension(BPOS,[max(BPOS,image(BPOS,reverse(BPOS,Seq),P1))]),empty_set(BPOS))). | |
| 916 | % indsOf[elm]: seq~[{elm}] | |
| 917 | sequence_function_to_b('seq\'indsOf',BPOS,[Seq,P1],image(BPOS,reverse(BPOS,Seq),set_extension(BPOS,[P1]))). | |
| 918 | % append[seq2]: LET x BE x = s^s2 IN (IF size(x) < MAXSEQ THEN x ELSE x /|\ MAXSEQ END) END | |
| 919 | % TO DO: use let like let_expression(BPOS,[identifier(BPOS,x)],equal(BPOS,identifier(BPOS,x),concat(Seq,P1)),if_then_else(BPOS,less_equal(BPOS,size(BPOS,identifier(BPOS,x)),integer(BPOS,MaxSeq)),identifier(BPOS,x),restrict_front(BPOS,identifier(BPOS,x),integer(BPOS,MaxSeq)))) | |
| 920 | sequence_function_to_b('seq\'append',BPOS,[Seq,P1],let_expression(BPOS,[identifier(BPOS,x)],equal(BPOS,identifier(BPOS,x),concat(Seq,P1)),if_then_else(BPOS,less_equal(BPOS,size(BPOS,identifier(BPOS,x)),integer(BPOS,MaxSeq)),identifier(BPOS,x),restrict_front(BPOS,identifier(BPOS,x),integer(BPOS,MaxSeq))))) :- | |
| 921 | maxseq(MaxSeq). | |
| 922 | % add[elm]: IF size(seq) < MAXSEQ THEN seq <- elm ELSE seq END | |
| 923 | sequence_function_to_b('seq\'add',BPOS,[Seq,P1],if_then_else(BPOS,less(BPOS,size(BPOS,Seq),integer(BPOS,MaxSeq)),insert_tail(BPOS,Seq,P1),Seq)) :- | |
| 924 | maxseq(MaxSeq). | |
| 925 | % delete[i]: IF (i >= 0 & i < size(seq)) THEN (seq /|\ i) ^ (seq \|/ i+1) ELSE seq END | |
| 926 | sequence_function_to_b('seq\'delete',BPOS,[Seq,P1],if_then_else(BPOS,conjunct(BPOS,greater_equal(BPOS,P1,integer(BPOS,0)),less(BPOS,P1,size(BPOS,Seq))),concat(BPOS,restrict_front(BPOS,Seq,P1),restrict_tail(BPOS,Seq,add(BPOS,P1,integer(BPOS,1)))),Seq)). | |
| 927 | % Sequence function calls with two parameters and the sequence itself. | |
| 928 | % setAt[i,elm]: IF (i >= 0 & i < size(seq)) THEN (seq /|\ i) ^ [elm] ^ (seq \|/ i+1) ELSE seq END | |
| 929 | sequence_function_to_b('seq\'setAt',BPOS,[Seq,P1,P2],if_then_else(BPOS,conjunct(BPOS,greater_equal(BPOS,P1,integer(BPOS,0)),less(BPOS,P1,size(BPOS,Seq))),concat(concat(BPOS,restrict_front(BPOS,Seq,P1),sequence_extension(BPOS,[P2])),restrict_tail(BPOS,Seq,add(BPOS,P1,integer(BPOS,1)))),Seq)). | |
| 930 | % insert[i,elm]: LET x BE x = (IF size(seq) = MAXSEQ THEN seq /|\ (MAXSEQ - 1) ELSE seq END) IN (x /|\ i) ^ [elm] ^ (x \|/ i) END | |
| 931 | sequence_function_to_b('seq\'insert',BPOS,[Seq,P1,P2],let_expression(BPOS,[identifier(BPOS,x)],equal(BPOS,identifier(BPOS,x),if_then_else(BPOS,equal(BPOS,size(BPOS,Seq),integer(BPOS,MaxSeq)),restrict_front(BPOS,Seq,minus(BPOS,integer(BPOS,MaxSeq),integer(BPOS,1))),Seq)),concat(concat(BPOS,restrict_front(BPOS,Seq,P1),sequence_extension(BPOS,[P2])),restrict_tail(BPOS,Seq,add(BPOS,P1,integer(BPOS,1)))))) :- | |
| 932 | maxseq(MaxSeq). | |
| 933 | % subseq[from,to]: IF 0 <= from & from <= to & to < size(seq) THEN (s \|/ from) /|\ ((to-from)+1) ELSE seq end | |
| 934 | sequence_function_to_b('seq\'subseq',BPOS,[Seq,P1,P2],if_then_else(BPOS,conjunct(BPOS,conjunct(BPOS,less_equal(BPOS,integer(BPOS,0),P1),less_equal(BPOS,P1,P2)),less(BPOS,P2,size(BPOS,Seq))),restrict_front(BPOS,restrict_tail(BPOS,Seq,P1),add(BPOS,minus(BPOS,P2,P1),integer(BPOS,1))))). | |
| 935 | ||
| 936 | sequence_function_to_b_functor(Name,BFunctor) :- | |
| 937 | atom_concat('seq\'',Functor,Name) , | |
| 938 | sequence_function_to_b_functor_aux(Functor,BFunctor). | |
| 939 | ||
| 940 | sequence_function_to_b_functor_aux(first,first). | |
| 941 | sequence_function_to_b_functor_aux(last,last). | |
| 942 | sequence_function_to_b_functor_aux(rest,tail). | |
| 943 | sequence_function_to_b_functor_aux(elems,range). | |
| 944 | ||
| 945 | translate_seq_function_param(join(identifier(this,type([Type],1),IPos),Arg2,JType,JPos),TParam) :- ! , | |
| 946 | % remove join with this for signature fields | |
| 947 | translate_e_p(join(identifier(Type,type([Type],1),IPos),Arg2,JType,JPos),TParam). | |
| 948 | translate_seq_function_param(Param,TParam) :- | |
| 949 | translate_e_p(Param,TParam). | |
| 950 | ||
| 951 | ||
| 952 | % sequence function calls: first, last, rest, elems | |
| 953 | translate_function_call(Name,[Param],_Type,BPOS,TCall) :- | |
| 954 | sequence_function_to_b_functor(Name,BFunctor) , ! , | |
| 955 | translate_seq_function_param(Param,TParam) , | |
| 956 | TCall =.. [BFunctor,BPOS,TParam]. | |
| 957 | translate_function_call(Function,Params,_Type,BPOS,TCall) :- | |
| 958 | maplist(translate_seq_function_param,Params,TParams) , | |
| 959 | sequence_function_to_b(Function,BPOS,TParams,TCall) , !. | |
| 960 | translate_function_call(Name,Params,Type,BPOS,Result) :- | |
| 961 | alloy_to_b_relational_utility_function(Name,Params,Type,BPOS,Result). | |
| 962 | translate_function_call(Name,Params,_Type,BPOS,Result) :- | |
| 963 | length(Params,Arity), | |
| 964 | alloy_utility_function(Name,Arity,BOp,ArgType,ReturnType) , !, % functions like plus, minus, mul, ... with integer arguments and result | |
| 965 | (ArgType = integer -> | |
| 966 | maplist(translate_e_p_integer,Params,TParams) | |
| 967 | ; maplist(translate_e_p,Params,TParams)), | |
| 968 | (ReturnType = integer -> | |
| 969 | Result = set_extension(BPOS,[TCall]) % we add set_extension wrapper | |
| 970 | ; Result = TCall), | |
| 971 | TCall =.. [BOp,BPOS|TParams]. | |
| 972 | % ordering function calls | |
| 973 | translate_function_call(FunName,Params,type([SignatureName|_],_),BPOS,TCall) :- | |
| 974 | translate_e_p(SignatureName,TSignatureName) , | |
| 975 | get_clean_ordering_fun_name(FunName,CleanOrdFunName) , | |
| 976 | translate_ordering_function(CleanOrdFunName,Params,SignatureName,TSignatureName,BPOS,TCall). | |
| 977 | translate_function_call(Name,Params,_,BPOS,TCall) :- | |
| 978 | % predicate and function call | |
| 979 | maplist(translate_e_p,Params,TParams) , | |
| 980 | maplist(strip_singleton_set_from_this,TParams,TTParams) , % identifier 'this' is added for fields which is already wrapped in a set extension | |
| 981 | TCall = definition(BPOS,Name,TTParams). | |
| 982 | ||
| 983 | % first: IF S_ord /= {} THEN {min(S_ord)} ELSE {} | |
| 984 | translate_ordering_function(first,[],_,TSignatureName,BPOS,if_then_else(BPOS,not_equal(BPOS,TSignatureName,empty_set(BPOS)),set_extension(BPOS,[min(BPOS,TSignatureName)]),empty_set(BPOS))) :- !. | |
| 985 | % last: IF S_ord /= {} THEN {max(S_ord)} ELSE {} | |
| 986 | translate_ordering_function(last,[],_,TSignatureName,BPOS,if_then_else(BPOS,not_equal(BPOS,TSignatureName,empty_set(BPOS)),set_extension(BPOS,[max(BPOS,TSignatureName)]),empty_set(BPOS))) :- !. | |
| 987 | % min[p]: IF p /= {} THEN {min(p)} ELSE {} | |
| 988 | % max[p]: IF p /= {} THEN {min(p)} ELSE {} | |
| 989 | translate_ordering_function(FunName,[Param],_,_,BPOS,TCall) :- | |
| 990 | (FunName == min ; FunName == max) , ! , | |
| 991 | translate_e_p(Param,TParam) , | |
| 992 | InnerCall =.. [FunName,BPOS,TParam] , | |
| 993 | TCall = if_then_else(BPOS,not_equal(BPOS,TParam,empty_set(BPOS)),set_extension(BPOS,[InnerCall]),empty_set(BPOS)). | |
| 994 | translate_ordering_function(FunName,[Param],SignatureName,_,BPOS,TCall) :- | |
| 995 | (FunName == next ; FunName == nexts ; FunName == prev ; FunName == prevs) , ! , | |
| 996 | get_ordering_definition_name(FunName,SignatureName,DefName) , | |
| 997 | translate_e_p(Param,TParam) , | |
| 998 | TCall = definition(BPOS,DefName,[TParam]). | |
| 999 | % larger[p1,p1]: IF p1 \/ p2 /= {} THEN {max(p1 \/ p2)} ELSE {} END | |
| 1000 | % smaller[p1,p2]: IF p1 \/ p2 /= {} THEN {min(p1 \/ p2)} ELSE {} END | |
| 1001 | translate_ordering_function(FunName,[P1,P2],_,_,BPOS,TCall) :- | |
| 1002 | (FunName == larger ; FunName == smaller) , | |
| 1003 | get_partial_b_functor_for_ordering(FunName,BFunctor) , | |
| 1004 | translate_e_p(P1,TP1) , | |
| 1005 | translate_e_p(P2,TP2) , | |
| 1006 | ParamUnion = union(BPOS,TP1,TP2) , | |
| 1007 | TInnerCall =.. [BFunctor,BPOS,ParamUnion] , | |
| 1008 | InnerCall = set_extension(BPOS,[TInnerCall]) , | |
| 1009 | TCall = if_then_else(BPOS,not_equal(BPOS,ParamUnion,empty_set(BPOS)),InnerCall,empty_set(BPOS)). | |
| 1010 | % lt[p1,p2]: (p1 = {}) or (p1 /= {} & p2 /= {} & p1 /= p2 & {min(p1 \/ p2)} = p1)) | |
| 1011 | % gt[p1,p2]: (p1 = {}) or (p1 /= {} & p2 /= {} & p1 /= p2 & {max(p1 \/ p2)} = p1)) | |
| 1012 | translate_ordering_function(FunName,[P1,P2],_,_,BPOS,TCall) :- | |
| 1013 | (FunName == lt ; FunName == gt) , | |
| 1014 | get_partial_b_functor_for_ordering(FunName,BFunctor) , | |
| 1015 | translate_e_p(P1,TP1) , | |
| 1016 | translate_e_p(P2,TP2) , | |
| 1017 | TInnerCall =.. [BFunctor,BPOS,union(BPOS,TP1,TP2)] , | |
| 1018 | InnerCall = set_extension(BPOS,[TInnerCall]) , | |
| 1019 | LHS = equal(BPOS,TP1,empty_set(BPOS)) , | |
| 1020 | RHS = conjunct(BPOS,conjunct(BPOS,conjunct(BPOS,not_equal(BPOS,TP1,empty_set(BPOS)),not_equal(BPOS,TP2,empty_set(BPOS))),not_equal(BPOS,TP1,TP2)),equal(BPOS,InnerCall,TP1)) , | |
| 1021 | TCall = disjunct(BPOS,LHS,RHS). | |
| 1022 | % lte[p1,p2]: (p1 = {}) or (p1 /= {} & p2 /= {} & {min(p1 \/ p2)} = p1) | |
| 1023 | % gte[p1,p2]: (p1 = {}) or (p1 /= {} & p2 /= {} & {max(p1 \/ p2)} = p1) | |
| 1024 | translate_ordering_function(FunName,[P1,P2],_,_,BPOS,TCall) :- | |
| 1025 | (FunName == lte ; FunName == gte) , | |
| 1026 | get_partial_b_functor_for_ordering(FunName,BFunctor) , | |
| 1027 | translate_e_p(P1,TP1) , | |
| 1028 | translate_e_p(P2,TP2) , | |
| 1029 | TInnerCall =.. [BFunctor,BPOS,union(BPOS,TP1,TP2)] , | |
| 1030 | InnerCall = set_extension(BPOS,[TInnerCall]) , | |
| 1031 | LHS = equal(BPOS,TP1,empty_set(BPOS)) , | |
| 1032 | RHS = conjunct(BPOS,conjunct(BPOS,not_equal(BPOS,TP1,empty_set(BPOS)),not_equal(BPOS,TP2,empty_set(BPOS))),equal(BPOS,InnerCall,TP1)) , | |
| 1033 | TCall = disjunct(BPOS,LHS,RHS). | |
| 1034 | translate_ordering_function(FunName,_,_,_,BPOS,empty_set(BPOS)) :- | |
| 1035 | add_error(translate_ordering_function,'Cannot translate ordering function',[FunName],BPOS). | |
| 1036 | ||
| 1037 | get_partial_b_functor_for_ordering(larger,max). | |
| 1038 | get_partial_b_functor_for_ordering(smaller,min). | |
| 1039 | get_partial_b_functor_for_ordering(lt,min). | |
| 1040 | get_partial_b_functor_for_ordering(lte,min). | |
| 1041 | get_partial_b_functor_for_ordering(gt,max). | |
| 1042 | get_partial_b_functor_for_ordering(gte,max). | |
| 1043 | ||
| 1044 | strip_singleton_set(set_extension(_,[identifier(Pos,Name)]),identifier(Pos,Name)) :- !. | |
| 1045 | strip_singleton_set(A,A). | |
| 1046 | ||
| 1047 | strip_singleton_set_from_this(set_extension(_,[identifier(Pos,this)]),identifier(Pos,this)) :- !. | |
| 1048 | strip_singleton_set_from_this(A,A). | |
| 1049 | ||
| 1050 | translate_cartesian(TPos,Arg1,Arg2,Res) :- | |
| 1051 | translate_e_p(Arg1,TArg1), | |
| 1052 | translate_cartesian2(TPos,TArg1,Arg2,Res). | |
| 1053 | ||
| 1054 | translate_cartesian2(TPos,TArg1,Arg2,Res) :- | |
| 1055 | translate_e_p(Arg2,TArg2), | |
| 1056 | translate_cartesian3(TPos,TArg1,Arg2,TArg2,Res). | |
| 1057 | % P -> Q --> P*Q | |
| 1058 | translate_cartesian3(TPos,TArg1,Arg2,TArg2,cartesian_product(TPos,TArg1,TArg2)) :- | |
| 1059 | is_unary_relation(Arg2), | |
| 1060 | !. | |
| 1061 | % P -> Q --> {c0, c1,...,ck | c0:P & (c1,...,ck):Q} | |
| 1062 | translate_cartesian3(TPos,TArg1,Arg2,TArg2,comprehension_set(TPos,[ID0|IDs2],conjunct(TPos,Mem1,Mem2))) :- | |
| 1063 | get_type_and_arity_from_alloy_term(Arg2,_Type,Arity), | |
| 1064 | gen_ids_and_couple(Arity,IDs2,Couple2), | |
| 1065 | gen_identifier(0,"_c_",ID0), | |
| 1066 | Mem1 = member(TPos,ID0,TArg1), | |
| 1067 | Mem2 = member(TPos,Couple2,TArg2). | |
| 1068 | ||
| 1069 | gen_ids_and_couple(Arity,[ID1|IDListRest],NestedCouple) :- | |
| 1070 | Arity>0, | |
| 1071 | gen_identifier(1,"_c_",ID1), | |
| 1072 | gen_ids_and_couple(2,Arity,IDListRest,ID1,NestedCouple). | |
| 1073 | ||
| 1074 | gen_ids_and_couple(Nr,Arity,L,Acc,Res) :- Nr>Arity,!, L=[], Res=Acc. | |
| 1075 | gen_ids_and_couple(Nr,Arity,[IDN|T],Acc,Res) :- | |
| 1076 | gen_identifier(Nr,"_c_",IDN), | |
| 1077 | N1 is Nr+1, | |
| 1078 | gen_ids_and_couple(N1,Arity,T,couple(none,Acc,IDN),Res). | |
| 1079 | ||
| 1080 | gen_identifier(Nr,Prefix,identifier(none,ID)) :- | |
| 1081 | number_codes(Nr,NrC), | |
| 1082 | append(Prefix,NrC,AC), | |
| 1083 | atom_codes(ID,AC). | |
| 1084 | ||
| 1085 | % ordering function calls like s.next.next are converted to fun_call | |
| 1086 | translate_join(_,Arg1,Arg2,TBinaryJoin) :- | |
| 1087 | Arg2 = fun_call(Name,[],Type,A2Pos) , | |
| 1088 | \+ atom_concat('integer',_,Name) , | |
| 1089 | translate_e_p(fun_call(Name,[Arg1],Type,A2Pos),TBinaryJoin). | |
| 1090 | % Translation of the dot join operator has several special cases depending on the arity of the arguments. | |
| 1091 | translate_join(Pos,Arg1,Arg2,TBinaryJoin) :- | |
| 1092 | translate_e_p(Arg1,TArg1), | |
| 1093 | translate_e_p(Arg2,TArg2), | |
| 1094 | %print(translate_join(Arg1,Arg2)),nl, | |
| 1095 | translate_join_aux(Pos,Arg1,Arg2,TArg1,TArg2,TBinaryJoin). | |
| 1096 | ||
| 1097 | % Note: N-ary relation are encoded in B as follows: | |
| 1098 | % { (e1 |-> (e2 |-> (e3 |-> ...))) ,... }, for example: | |
| 1099 | % {(tracy|->(spanish|->french)),(carol|->(spanish|->french)), ...} | |
| 1100 | ||
| 1101 | % univ.P --> ran(P) % this does NOT work for ternary,... relations | |
| 1102 | translate_join_aux(TPos,Arg1,Arg2,_TArg1,TArg2,range(TPos,TArg2)) :- | |
| 1103 | is_univ(Arg1), | |
| 1104 | is_binary_relation(Arg2), | |
| 1105 | !. | |
| 1106 | % P.univ --> dom(P) % this works for ternary,... relations | |
| 1107 | translate_join_aux(TPos,_Arg1,Arg2,TArg1,_TArg2,domain(TPos,TArg1)) :- | |
| 1108 | is_univ(Arg2), | |
| 1109 | !. | |
| 1110 | % {el}.R --> {R(el)} | |
| 1111 | translate_join_aux(Pos,Arg1,Arg2,TArg1,TArg2,set_extension(Pos,[function(Pos,TArg2,[TTArg1])])) :- | |
| 1112 | get_type_and_arity_from_alloy_term(Arg1,Type1,Arity), Arity=1, %is_unary_relation(Arg1), | |
| 1113 | is_binary_relation(Arg2), | |
| 1114 | is_total_function(TArg2,Type1), | |
| 1115 | can_remove_singleton_set(TArg1,TTArg1), | |
| 1116 | !. | |
| 1117 | % unary.R --> R[unary] | |
| 1118 | translate_join_aux(Pos,Arg1,Arg2,TArg1,TArg2,image(Pos,TArg2,TArg1)) :- % Unary.Arg2 --> Arg2[Unary] | |
| 1119 | is_unary_relation(Arg1), | |
| 1120 | is_binary_relation(Arg2), | |
| 1121 | !. | |
| 1122 | % binary.unary | |
| 1123 | % Next RULE is broken, can lead to Type errors and test is wrong: | |
| 1124 | %translate_join_aux(Pos,Arg1,Arg2,TArg1,TArg2,function(Pos,reverse(Pos,TArg1),[TTArg2])) :- | |
| 1125 | % % function call if lhs is a total function and rhs a unary relation | |
| 1126 | % is_binary_relation(Arg1), | |
| 1127 | % is_unary_relation(Arg2), | |
| 1128 | % is_total_function(TArg1) , ! , % TEST SHOULD BE SURJECTIVE and INJECTIVE !! | |
| 1129 | % remove_singleton_set(TArg2,TTArg2). | |
| 1130 | % Arg1.Unary --> Arg1~[Unary] | |
| 1131 | translate_join_aux(Pos,_Arg1,Arg2,TArg1,TArg2,image(Pos,reverse(Pos,TArg1),TArg2)) :- | |
| 1132 | is_unary_relation(Arg2), | |
| 1133 | !. | |
| 1134 | % binary.binary: Arg1.Arg2 --> (Arg1 ; Arg2) | |
| 1135 | translate_join_aux(Pos,Arg1,Arg2,TArg1,TArg2,composition(Pos,TArg1,TArg2)) :- | |
| 1136 | is_binary_relation(Arg1), | |
| 1137 | is_binary_relation(Arg2), | |
| 1138 | !. | |
| 1139 | translate_join_aux(Pos,Arg1,Arg2,TArg1,TArg2,comprehension_set(Pos,IDS,Body)) :- | |
| 1140 | Body = conjunct(Pos,TypingPred,exists(Pos,[JoinID],conjunct(Pos,JoinTypingPred,conjunct(Pos,Mem1,Mem2)))), | |
| 1141 | get_type_and_arity_from_alloy_term(Arg2,[JoinIDType|RTypes],Arity), % first type refers to outter variable | |
| 1142 | gen_ids_and_couple(Arity,IDs2,Couple2), IDs2 = [JoinID|Rest2], | |
| 1143 | get_typing_pred_for_ids(Pos,RTypes,Rest2,TypingPred) , | |
| 1144 | get_typing_pred_for_ids(Pos,[JoinIDType],[JoinID],JoinTypingPred) , | |
| 1145 | (is_univ(Arg1) -> | |
| 1146 | Mem1 = truth(TPos), IDS=Rest2 | |
| 1147 | ; is_unary_relation(Arg1) -> | |
| 1148 | strip_singleton_set_from_this(TArg1,TTArg1) , | |
| 1149 | Mem1 = member(TPos,JoinID,TTArg1), | |
| 1150 | IDS = Rest2 | |
| 1151 | ; gen_identifier(0,"_c_",ID0), | |
| 1152 | IDS = [ID0|Rest2], | |
| 1153 | Mem1 = member(TPos,couple(TPos,ID0,JoinID),TArg1) | |
| 1154 | ), | |
| 1155 | Mem2 = member(TPos,Couple2,TArg2). | |
| 1156 | translate_join_aux(Pos,Arg1,Arg2,_TArg1,_TArg2,empty_set(Pos)) :- | |
| 1157 | format('~nJoin not supported this way:~nLeft: ~w~nRight: ~w~n',[Arg1,Arg2]), | |
| 1158 | add_error(load_alloy_model,'Cannot translate this type of join yet',[Arg1,Arg2],Pos). | |
| 1159 | ||
| 1160 | % This predicate relies on the order of elements in 2. and 3. argument for typing. | |
| 1161 | % TO DO: improve | |
| 1162 | get_typing_pred_for_ids(Pos,[],[],truth(Pos)). | |
| 1163 | get_typing_pred_for_ids(Pos,[Type|TT],[ID|IT],TypingPred) :- | |
| 1164 | translate_e_p(Type,TType) , | |
| 1165 | get_typing_pred_for_ids_acc(Pos,TT,IT,member(Pos,ID,TType),TypingPred). | |
| 1166 | ||
| 1167 | get_typing_pred_for_ids_acc(_,[],[],Acc,Acc). | |
| 1168 | get_typing_pred_for_ids_acc(Pos,[Type|TT],[ID|IT],Acc,TypingPred):- | |
| 1169 | translate_e_p(Type,TType) , | |
| 1170 | get_typing_pred_for_ids_acc(Pos,TT,IT,conjunct(Pos,Acc,member(Pos,ID,TType)),TypingPred). | |
| 1171 | ||
| 1172 | % translate Alloy position to B position | |
| 1173 | translate_pos(pos(Col,Row),Res) :- !, Res=pos(0,1,Row,Col,Row,Col). | |
| 1174 | translate_pos(_,none). | |
| 1175 | ||
| 1176 | get_position(Term,BPos) :- functor(Term,_,Arity), Arity>0, arg(Arity,Term,Pos), !,translate_pos(Pos,BPos). | |
| 1177 | get_position(_,none). | |
| 1178 | ||
| 1179 | translate_quantified_e(Pos,no,TArg,equal(Pos,TArg,empty_set(none))). | |
| 1180 | translate_quantified_e(Pos,one,TArg,equal(Pos,card(none,TArg),integer(none,1))). | |
| 1181 | translate_quantified_e(Pos,some,TArg,greater(Pos,card(none,TArg),integer(none,0))). | |
| 1182 | translate_quantified_e(Pos,lone,TArg,less_equal(Pos,card(none,TArg),integer(none,1))). | |
| 1183 | ||
| 1184 | % Join a list of types using cartesian_product like ((A*B)*C) for types [A,B,C]. | |
| 1185 | create_cartesian_type([ID],TID) :- ! , | |
| 1186 | translate_unary_e_p(ID,TID). | |
| 1187 | create_cartesian_type([ID1,ID2],cartesian_product(none,TID1,TID2)) :- ! , | |
| 1188 | translate_unary_e_p(ID1,TID1) , | |
| 1189 | translate_unary_e_p(ID2,TID2). | |
| 1190 | create_cartesian_type([ID1,ID2|T],cartesian_product(none,cartesian_product(none,TID1,TID2),NT)) :- | |
| 1191 | translate_unary_e_p(ID1,TID1) , | |
| 1192 | translate_unary_e_p(ID2,TID2) , | |
| 1193 | create_cartesian_type(T,NT). | |
| 1194 | ||
| 1195 | % Field declarations have several special cases depending on the keywords set, one, some or lone. | |
| 1196 | % We are inside Signature TSignatureName sig NAME { field : DeclTerm } | |
| 1197 | translate_field_decl(BPOS,SignatureName,TSignatureName,DeclTerm,FieldID,TFieldID,TFieldPred) :- | |
| 1198 | %DeclTerm =.. [_,SetID|_], | |
| 1199 | replace_this_in_signature_field(DeclTerm,NewDeclTerm), | |
| 1200 | format('Translating Field ~w inside signature ~w,~n Term=~w,~n~n',[FieldID,SignatureName,NewDeclTerm]), | |
| 1201 | (translate_special_multiplicity_binary_e_p(NewDeclTerm,TFUNC) | |
| 1202 | -> %we could do: translate_cartesian2(BPOS,TSignatureName,NewDeclTerm,Cart), TFieldPred = subset(BPOS,TFieldID,Cart), and add predicate | |
| 1203 | % TO DO: better treatment, also detect nested special multiplicity annotations inside NewDeclTerm | |
| 1204 | ||
| 1205 | % generate forall x:SIG => x.field : TFUNC | |
| 1206 | ID = identifier(BPOS,'_x_'), AID = identifier('_x_',type([SignatureName],1),none), | |
| 1207 | (singleton_set('_x_') -> true ; assert_singleton_set('_x_')), | |
| 1208 | translate_e_p(AID,TAID), % will add set-extension wrapper | |
| 1209 | LHS = member(BPOS,ID,TSignatureName), | |
| 1210 | RHS = member(BPOS,TJoin,TFUNC), | |
| 1211 | TFieldPred = conjunct(BPOS,FieldTyping,forall(BPOS,[ID],implication(none,LHS,RHS))), | |
| 1212 | translate_join_aux(BPOS,AID,FieldID,TAID,TFieldID,TJoin), | |
| 1213 | get_type_and_arity_from_alloy_term(FieldID,TypeList,_) , | |
| 1214 | create_cartesian_type(TypeList,CartesianType) , | |
| 1215 | FieldTyping = member(Pos,TFieldID,pow_subset(Pos,CartesianType)) | |
| 1216 | ; translate_sig_field_rhs(FieldID,NewDeclTerm,BPOS,TSignatureName,TFieldID,FieldTypeExpr) | |
| 1217 | -> add_constraint_for_someof_field(NewDeclTerm,member(BPOS,TFieldID,FieldTypeExpr),TFieldPred) | |
| 1218 | ; add_error(alloy2b,'Field declaration not implemented:',NewDeclTerm,BPOS), | |
| 1219 | TFieldPred = truth(none) | |
| 1220 | ). | |
| 1221 | ||
| 1222 | add_constraint_for_someof_field(someof(_,_,_),TempPred,conjunct(BPOS,not_equal(BPOS,TFieldID,empty_set(BPOS)),TempPred)) :- ! , | |
| 1223 | TempPred = member(BPOS,TFieldID,_). | |
| 1224 | add_constraint_for_someof_field(_,Pred,Pred). | |
| 1225 | ||
| 1226 | % sig SIG { field : set Set} --> field : SIG <-> Set | |
| 1227 | translate_sig_field_rhs(_,setof(Set,_,_),_,SIG,_,relations(none,SIG,TSet)) :- | |
| 1228 | translate_e_p(Set,TSet). | |
| 1229 | % sig SIG { field : one Set} --> field : SIG --> Set | |
| 1230 | translate_sig_field_rhs(_,oneof(Set,_,_),_,SIG,TFieldID,total_function(none,SIG,TSet)) :- | |
| 1231 | translate_e_p(Set,TSet), | |
| 1232 | assert_total_function(TFieldID,SIG). | |
| 1233 | % sig SIG { field : lone Set} --> field : SIG +-> Set | |
| 1234 | translate_sig_field_rhs(_,loneof(Set,_,_),_,SIG,_,partial_function(none,SIG,TSet)) :- | |
| 1235 | translate_e_p(Set,TSet). | |
| 1236 | % sig SIG { field : some Set} --> field : SIG +-> Set | |
| 1237 | translate_sig_field_rhs(_,someof(Set,_,_),_,SIG,_,relations(none,SIG,TSet)) :- | |
| 1238 | translate_e_p(Set,TSet). | |
| 1239 | % sig SIG { field : seq Set} --> field : (SIG * Integer) +-> Set | |
| 1240 | translate_sig_field_rhs(FieldID,'isseq->lone'(_,Set,_,_),_,SIG,_,partial_function(none,cartesian_product(none,SIG,integer_set(none,'INTEGER')),TSet)) :- | |
| 1241 | assert(is_seq(FieldID)) , | |
| 1242 | translate_e_p(Set,TSet). | |
| 1243 | % sig SIG { field : FieldTerm} --> field : POW(SIG * FieldTerm) | |
| 1244 | translate_sig_field_rhs(_,FieldTerm,Pos,SIG,_,pow_subset(none,Cart)) :- | |
| 1245 | % TO DO: check whether lone, one, ... can appear inside FieldTerm | |
| 1246 | translate_cartesian2(Pos,SIG,FieldTerm,Cart). | |
| 1247 | ||
| 1248 | replace_this_in_signature_field(identifier('this',type([SignatureName],1),Pos),Res) :- !, | |
| 1249 | Res = identifier(SignatureName,type([SignatureName],1),Pos). | |
| 1250 | replace_this_in_signature_field(DeclTerm,NewDeclTerm) :- | |
| 1251 | DeclTerm =.. [Functor,Arg1,Type,Pos], !, | |
| 1252 | replace_this_in_signature_field(Arg1,NArg1) , | |
| 1253 | NewDeclTerm =.. [Functor,NArg1,Type,Pos]. | |
| 1254 | replace_this_in_signature_field(DeclTerm,NewDeclTerm) :- | |
| 1255 | DeclTerm =.. [Functor,Arg1,Arg2,Type,Pos], !, | |
| 1256 | replace_this_in_signature_field(Arg1,NArg1) , | |
| 1257 | replace_this_in_signature_field(Arg2,NArg2) , | |
| 1258 | NewDeclTerm =.. [Functor,NArg1,NArg2,Type,Pos]. | |
| 1259 | replace_this_in_signature_field(DeclTerm,DeclTerm). | |
| 1260 | ||
| 1261 | % Translate TFieldID: Declaration | |
| 1262 | fun_or_pred_decl_special_cases(setof(Expr,_,_),TFieldID,Pos,subset(Pos,TFieldID,TExpr),set) :- | |
| 1263 | translate_e_p(Expr,TExpr). | |
| 1264 | fun_or_pred_decl_special_cases(oneof(Expr,_,_),TFieldID,Pos,subset(Pos,TFieldID,TExpr),singleton) :- % Default | |
| 1265 | translate_e_p(Expr,TExpr). | |
| 1266 | fun_or_pred_decl_special_cases(loneof(Expr,_,_),TFieldID,Pos,conjunct(Pos,subset(Pos,TFieldID,TExpr),ExtraPred),set) :- | |
| 1267 | % x : lone S -> x <: S & card(x) <= 1 | |
| 1268 | ExtraPred = less_equal(Pos,card(Pos,TFieldID),integer(Pos,1)), | |
| 1269 | translate_e_p(Expr,TExpr). | |
| 1270 | fun_or_pred_decl_special_cases(someof(Expr,_,_),TFieldID,Pos,conjunct(Pos,subset(Pos,TFieldID,TExpr),ExtraPred),set) :- | |
| 1271 | % x : some S -> x <: S & x \= {} | |
| 1272 | ExtraPred = not_equal(Pos,TFieldID,empty_set(Pos)), | |
| 1273 | translate_e_p(Expr,TExpr). | |
| 1274 | fun_or_pred_decl_special_cases(Expr,TFieldID,Pos,Translation,IsSingleton) :- | |
| 1275 | % treat identifier, cartesian, union, ... use translate of TFieldID in Expr | |
| 1276 | translate_binary_in(TFieldID,Expr,Pos,Translation), | |
| 1277 | get_type_and_arity_from_alloy_term(Expr,_Type,Arity), | |
| 1278 | !, | |
| 1279 | (Arity=1 -> IsSingleton = singleton ; IsSingleton = set). | |
| 1280 | fun_or_pred_decl_special_cases(Term,_,Pos,falsity(Pos),set) :- | |
| 1281 | add_error(alloy2b,'Field declaration for function or predicate not implemented:',Term,Pos). | |
| 1282 | ||
| 1283 | alloy_to_b_operator(Op,BOp) :- | |
| 1284 | alloy_to_b_unary_operator(Op,BOp) , !. | |
| 1285 | alloy_to_b_operator(Op,BOp) :- | |
| 1286 | alloy_to_b_binary_operator(Op,BOp) , !. | |
| 1287 | alloy_to_b_operator(Op,Op) :- format('~n~nTRANSLATING ~w to B without modification!~n',[Op]). | |
| 1288 | ||
| 1289 | alloy_to_b_unary_operator(not,negation). | |
| 1290 | alloy_to_b_unary_operator(closure1,closure). | |
| 1291 | alloy_to_b_unary_operator(closure,reflexive_closure). | |
| 1292 | alloy_to_b_unary_operator(inverse,reverse). % works for binary relation only; indeed Alloy says: ~ can be used only with a binary relation. | |
| 1293 | ||
| 1294 | ||
| 1295 | alloy_to_b_binary_operator(in,subset). | |
| 1296 | alloy_to_b_binary_operator(not_in,not_subset). | |
| 1297 | alloy_to_b_binary_operator(plus,union). | |
| 1298 | alloy_to_b_binary_operator(or,disjunct). % actually treated as unary operator | |
| 1299 | alloy_to_b_binary_operator(and,conjunct). % actually treated as unary operator | |
| 1300 | alloy_to_b_binary_operator(minus,set_subtraction). | |
| 1301 | %alloy_to_b_binary_operator(cartesian,cartesian_product). % only works for X->UNARY ! | |
| 1302 | alloy_to_b_binary_operator(function,expression_definition). | |
| 1303 | alloy_to_b_binary_operator(predicate,predicate_definition). | |
| 1304 | alloy_to_b_binary_operator(not_equal,not_equal). | |
| 1305 | alloy_to_b_binary_operator(dom_restr,domain_restriction). % not ok for ternary, set must be unary | |
| 1306 | alloy_to_b_binary_operator(ran_restr,range_restriction). % also ok for ternary, ... relations | |
| 1307 | alloy_to_b_binary_operator(equal,equal). | |
| 1308 | alloy_to_b_binary_operator(conjunct,conjunct). | |
| 1309 | alloy_to_b_binary_operator(intersection,intersection). | |
| 1310 | alloy_to_b_binary_operator(implication,implication). | |
| 1311 | alloy_to_b_binary_operator(iff,equivalence). | |
| 1312 | alloy_to_b_binary_operator(override,overwrite). % ++ | |
| 1313 | ||
| 1314 | is_cartesian_product_term(Term,Arg1,Arg2,POS) :- functor(Term,Functor,4), | |
| 1315 | is_cartesian_product(Functor), | |
| 1316 | arg(1,Term,Arg1), arg(2,Term,Arg2), arg(4,Term,POS). | |
| 1317 | is_cartesian_product(cartesian). | |
| 1318 | is_cartesian_product(Special) :- % translate as Cartesian product for typing predicates ONLY ! (generates unsound translations on its own, needs to be augmented with predicates which check the multiplicity !) | |
| 1319 | alloy_to_b_special_multiplicity_type(Special,_,_,_,POS), | |
| 1320 | translate_pos(POS,BPOS), | |
| 1321 | add_warning(alloy2b,'Treating operator as Cartesian product (cannot translate nested multiplicity in signature yet):',Special,BPOS). | |
| 1322 | ||
| 1323 | alloy_to_b_special_multiplicity_type(total_function,total_function,set,one,ok). % TO DO: requires element rather than subset, fix, see birthday.als; can only be used in context of in, !in | |
| 1324 | alloy_to_b_special_multiplicity_type(partial_function,partial_function,set,lone,ok). | |
| 1325 | alloy_to_b_special_multiplicity_type(partial_injection,partial_injection,set,lone,ok). | |
| 1326 | alloy_to_b_special_multiplicity_type(total_bijection,total_bijection,one,one,ok). | |
| 1327 | alloy_to_b_special_multiplicity_type(total_injection,total_injection,lone,one,ok). | |
| 1328 | alloy_to_b_special_multiplicity_type(partial_surjection,partial_surjection,some,lone,ok). | |
| 1329 | alloy_to_b_special_multiplicity_type(total_surjection,total_surjection,some,one,ok). | |
| 1330 | % relations: | |
| 1331 | alloy_to_b_special_multiplicity_type(total_relation,total_relation,set,some,ok). | |
| 1332 | alloy_to_b_special_multiplicity_type(total_surjection_relation,total_surjection_relation,some,some,ok). | |
| 1333 | alloy_to_b_special_multiplicity_type(surjection_relation,surjection_relation,some,set,ok). | |
| 1334 | alloy_to_b_special_multiplicity_type(injection_relation,injection_relation,lone,set,not_supported). % "lone->" NOT SUPPORTED BY PROB | |
| 1335 | alloy_to_b_special_multiplicity_type(injection_surjection_relation,injection_surjection_relation,lone,some,not_supported). % "lone->some" NOT SUPPORTED BY PROB | |
| 1336 | alloy_to_b_special_multiplicity_type(total_bijection_relation,total_bijection_relation,one,some,not_supported). % "one->some" NOT SUPPORTED BY PROB | |
| 1337 | alloy_to_b_special_multiplicity_type(total_bijection_relation,bijection_relation,one,set,not_supported). % "one->" NOT SUPPORTED BY PROB | |
| 1338 | ||
| 1339 | ||
| 1340 | % predicates with integer arguments | |
| 1341 | alloy_to_b_integer_operator(less,less). | |
| 1342 | alloy_to_b_integer_operator(greater,greater). | |
| 1343 | alloy_to_b_integer_operator(less_equal,less_equal). | |
| 1344 | alloy_to_b_integer_operator(greater_equal,greater_equal). | |
| 1345 | ||
| 1346 | ||
| 1347 | %%% | |
| 1348 | % Accumulate the translated machine parts and signature names during the translation and build the machine AST afterwards. | |
| 1349 | % We may need the signature names later on if translating a global scope. | |
| 1350 | build_machine_ast(b_machine(ListOfMachineParts,_SignatureNames),machine(generated(none,AbstractMachine))) :- | |
| 1351 | % filter empty machine parts | |
| 1352 | findall(MachinePart,(member(MachinePart,ListOfMachineParts) , MachinePart =.. [_,_,L], | |
| 1353 | L \= []),NonEmptyMachineSections) , | |
| 1354 | % properties need to be conjoined | |
| 1355 | (select(properties(none,L),NonEmptyMachineSections,RestListOfUsedMachineParts) -> true | |
| 1356 | ; L=[], RestListOfUsedMachineParts=NonEmptyMachineSections), | |
| 1357 | join_predicates(conjunct,L,FlatL) , | |
| 1358 | AbstractMachine = abstract_machine(none,machine(none), | |
| 1359 | machine_header(none,alloytranslation,[]), | |
| 1360 | [properties(none,FlatL)|RestListOfUsedMachineParts]) , !. | |
| 1361 | ||
| 1362 | empty_machine_acc(b_machine([sets(none,[]),constants(none,[]), | |
| 1363 | definitions(none,[]),properties(none,[]), | |
| 1364 | assertions(none,[]),operations(none,[])],[])). | |
| 1365 | ||
| 1366 | % extend a machine section with a give list of conjuncts | |
| 1367 | extend_machine_with_conjuncts(_Section,[],Acc,Res) :- !, Res=Acc. | |
| 1368 | extend_machine_with_conjuncts(Section,Conjuncts,MAcc1,MAcc2) :- | |
| 1369 | join_untyped_ast_nodes(conjunct,Conjuncts,TPred), | |
| 1370 | extend_machine_acc(Section,MAcc1,TPred,MAcc2). | |
| 1371 | ||
| 1372 | extend_machine_acc(signatures,b_machine(MachineParts,SignatureNames),New, | |
| 1373 | b_machine(MachineParts,NewSignatureNames)) :- ! , | |
| 1374 | append(SignatureNames,New,TSignatureNames) , | |
| 1375 | remove_dups(TSignatureNames,NewSignatureNames). | |
| 1376 | extend_machine_acc(Functor,b_machine(MachineParts,SignatureNames),New, | |
| 1377 | b_machine([NewMachinePart|RestMachineParts],SignatureNames)) :- | |
| 1378 | MachinePart =.. [Functor,none,List] , | |
| 1379 | select(MachinePart,MachineParts,RestMachineParts), % print(add_new(Functor,New)),nl,nl, | |
| 1380 | append(List,[New],NewList), % keeps order, but is inefficient! | |
| 1381 | NewMachinePart =.. [Functor,none,NewList], !. | |
| 1382 | extend_machine_acc(Functor,_,_,_) :- | |
| 1383 | add_internal_error('Failed: ',extend_machine_acc(Functor,_,_,_) ),fail. | |
| 1384 | ||
| 1385 | get_signature_names_from_machine_acc(b_machine(_MachineParts,SignatureNames),SignatureNames). | |
| 1386 | ||
| 1387 | get_command_counter_atom(CommandCounterAtom) :- | |
| 1388 | command_counter(CommandCounter) , | |
| 1389 | number_codes(CommandCounter,CommandCounterCodes) , | |
| 1390 | atom_codes(CommandCounterAtom,CommandCounterCodes) , | |
| 1391 | retractall(command_counter(_)) , | |
| 1392 | NewCommandCounter is CommandCounter + 1 , | |
| 1393 | asserta(command_counter(NewCommandCounter)). | |
| 1394 | ||
| 1395 | finalize_extending_signatures(MAcc,NewMAcc) :- | |
| 1396 | extending_signatures(List), ! , | |
| 1397 | finalize_extending_signatures_aux(MAcc,List,NewMAcc). | |
| 1398 | finalize_extending_signatures(MAcc,MAcc). | |
| 1399 | ||
| 1400 | finalize_extending_signatures_aux(MAcc,[],MAcc). | |
| 1401 | finalize_extending_signatures_aux(MAcc,[(Parent,SubSigs)|T],NewMAcc) :- | |
| 1402 | length(SubSigs,AmountOfSubSigs) , | |
| 1403 | AmountOfSubSigs > 1 , ! , | |
| 1404 | maplist(translate_sub_sig,SubSigs,TSubSigs) , | |
| 1405 | translate_e_p(Parent,TParent) , | |
| 1406 | extend_machine_acc(properties,MAcc,partition(none,TParent,TSubSigs),MAcc2), | |
| 1407 | % equivalent to | |
| 1408 | % parent = sub1 \/ sub2 \/ ... \/ subN & sub1 /\ sub2 = {} & ... | |
| 1409 | findall(OneSub,member(OneSub/one,SubSigs),OneSubSigs), | |
| 1410 | length(OneSubSigs,AmountOneSubSigs), | |
| 1411 | (AmountOneSubSigs = AmountOfSubSigs % we basically have an enumerated set with only singleton elements | |
| 1412 | -> extend_machine_acc(properties,MAcc2,equal(none,card(none,TParent),integer(none,AmountOneSubSigs)),MAcc3) | |
| 1413 | ; extend_machine_acc(properties,MAcc2,greater_equal(none,card(none,TParent),integer(none,AmountOneSubSigs)),MAcc3) | |
| 1414 | ), | |
| 1415 | finalize_extending_signatures_aux(MAcc3,T,NewMAcc). | |
| 1416 | finalize_extending_signatures_aux(MAcc,[_|T],NewMAcc) :- | |
| 1417 | finalize_extending_signatures_aux(MAcc,T,NewMAcc). | |
| 1418 | %%% | |
| 1419 | ||
| 1420 | translate_sub_sig(Name/_One,B) :- translate_e_p(Name,B). | |
| 1421 | ||
| 1422 | assert_extending_signature(Name,Parent,One) :- | |
| 1423 | (is_sub_signature_of(Name,Parent,One) -> true | |
| 1424 | ; format('~w is sub signature of ~w (~w)~n',[Name,Parent,One]), | |
| 1425 | assert(is_sub_signature_of(Name,Parent,One))), | |
| 1426 | extending_signatures(List), | |
| 1427 | select((Parent,SubSigs),List,Rest), | |
| 1428 | !, | |
| 1429 | (\+ memberchk(Name/One,SubSigs) | |
| 1430 | -> retractall(extending_signatures(_)) , | |
| 1431 | asserta(extending_signatures([(Parent,[Name/One|SubSigs])|Rest])) | |
| 1432 | ; true). | |
| 1433 | assert_extending_signature(Name,Parent,One) :- | |
| 1434 | retract(extending_signatures(List)), | |
| 1435 | !, | |
| 1436 | asserta(extending_signatures([(Parent,[Name/One])|List])). | |
| 1437 | assert_extending_signature(Name,Parent,One) :- | |
| 1438 | asserta(extending_signatures([(Parent,[Name/One])])). | |
| 1439 | ||
| 1440 | assert_enumerated_set(Options,Name) :- | |
| 1441 | % singleton top-level signatures are defined as an enumerated set like S = {_S} | |
| 1442 | member(one,Options) , | |
| 1443 | % but extending singleton signatures are defined as constants and singleton subsets of their parent type | |
| 1444 | \+ member(subset(_),Options) , | |
| 1445 | \+ member(subsig(_),Options) , ! , | |
| 1446 | asserta(enumerated_set(Name)). | |
| 1447 | assert_enumerated_set(_,_). | |
| 1448 | ||
| 1449 | assert_singleton_set(Options,Name) :- | |
| 1450 | member(one,Options) , ! , | |
| 1451 | assert_singleton_set(Name). | |
| 1452 | assert_singleton_set(_,_). | |
| 1453 | ||
| 1454 | assert_singleton_set(Name) :- %format('Singleton set : ~w~n',[Name]),nl, | |
| 1455 | %\+ singleton_set(Name), | |
| 1456 | asserta(singleton_set(Name)), | |
| 1457 | !. | |
| 1458 | %assert_singleton_set(_). | |
| 1459 | ||
| 1460 | retract_singleton_set(BPOS,Name) :- | |
| 1461 | (retract(singleton_set(Name)) -> true ; | |
| 1462 | add_message(retract_singleton_set,'WARNING: no singleton_set fact for: ',Name,BPOS) % can be ok for non-singleton ids | |
| 1463 | ). | |
| 1464 | % retractall(singleton_set(Name)). | |
| 1465 | ||
| 1466 | retract_state :- | |
| 1467 | retractall(uses_seqs) , | |
| 1468 | retractall(enumerated_set(_)) , | |
| 1469 | retractall(current_command(_)) , | |
| 1470 | retractall(command_counter(_)) , | |
| 1471 | asserta(command_counter(0)) , | |
| 1472 | retractall(singleton_set(_)) , | |
| 1473 | retractall(ordered_signature(_)) , | |
| 1474 | retractall(total_function(_,_)) , | |
| 1475 | retractall(extending_signatures(_)) , | |
| 1476 | retractall(is_seq(_)) , | |
| 1477 | retractall(maxseq(_)) , | |
| 1478 | retractall(is_sub_signature_of(_,_,_)) , !. | |
| 1479 | ||
| 1480 | % an identifier which in B refers not to a set but an element of a set, representing a singleton set in Alloy | |
| 1481 | is_singleton_set_id(this). % this is always singleton (TO DO: check this ;-) | |
| 1482 | is_singleton_set_id(IDName) :- singleton_set(IDName). | |
| 1483 | ||
| 1484 | assert_total_function(identifier(_,Name),SIG) :- !, | |
| 1485 | assert_total_function(Name,SIG). | |
| 1486 | assert_total_function(Name,identifier(_,SIG)) :- !, | |
| 1487 | assert_total_function(Name,SIG). | |
| 1488 | assert_total_function(Name,SIG) :- format('Total function ~w over ~w~n',[Name,SIG]), | |
| 1489 | asserta(total_function(Name,SIG)). | |
| 1490 | ||
| 1491 | is_total_function(predecessor(_),_). % translation of prev | |
| 1492 | is_total_function(successor(_),_). % translation of next | |
| 1493 | is_total_function(function(_,ID,_),ArgType) :- !, | |
| 1494 | is_total_function(ID,ArgType). | |
| 1495 | is_total_function(identifier(_,Name),ArgType) :- !, | |
| 1496 | is_total_function(Name,ArgType). | |
| 1497 | is_total_function(Name,[ArgType]) :- | |
| 1498 | total_function(Name,FunType), % TO DO: check if FunctionType is Superset of ArgType | |
| 1499 | (strip_singleton_set(FunType,SFunType),SFunType=identifier(_,ArgType) | |
| 1500 | -> true | |
| 1501 | ; is_sub_signature_of(ArgType,FunType,_)). | |
| 1502 | ||
| 1503 | assert_ordered_sig_name(Name) :- | |
| 1504 | asserta(ordered_signature(Name)). | |
| 1505 | ||
| 1506 | is_ordered_signature(IDName) :- | |
| 1507 | ordered_signature(IDName). | |
| 1508 | is_ordered_signature('ordering\''). | |
| 1509 | ||
| 1510 | is_univ(identifier('univ',_,_)). % universe | |
| 1511 | ||
| 1512 | is_unary_relation(AlloyTerm) :- | |
| 1513 | get_type_and_arity_from_alloy_term(AlloyTerm,_Type,Arity) , | |
| 1514 | Arity == 1. | |
| 1515 | ||
| 1516 | is_binary_relation(AlloyTerm) :- | |
| 1517 | get_type_and_arity_from_alloy_term(AlloyTerm,_Type,Arity) , | |
| 1518 | Arity == 2. | |
| 1519 | ||
| 1520 | can_remove_singleton_set(set_extension(_,[Element]),Element). | |
| 1521 | %remove_singleton_set(AST,AST). | |
| 1522 | ||
| 1523 | get_type_and_arity_from_alloy_term(integer(_,_),Type,Arity) :- !, | |
| 1524 | Type=integer, Arity=1. % will get translated to singleton set | |
| 1525 | get_type_and_arity_from_alloy_term(and(_,_),Type,Arity) :- !, | |
| 1526 | Type=[untyped], Arity=0. % predicate | |
| 1527 | get_type_and_arity_from_alloy_term(or(_,_),Type,Arity) :- !, | |
| 1528 | Type=[untyped], Arity=0. % predicate | |
| 1529 | get_type_and_arity_from_alloy_term(iden(_),Type,Arity) :- !, | |
| 1530 | Type=univ, Arity=2. | |
| 1531 | get_type_and_arity_from_alloy_term(AlloyTerm,Type,NArity) :- | |
| 1532 | AlloyTerm =.. [_|Args] , | |
| 1533 | member(type(Type,Arity),Args) , | |
| 1534 | (is_primitive_type(Type,NArity) ; | |
| 1535 | (length(Type,LType) , LType == Arity , NArity = Arity)) , | |
| 1536 | !. | |
| 1537 | get_type_and_arity_from_alloy_term(AlloyTerm,Type,Arity) :- | |
| 1538 | add_warning(alloy2b,'Could not extract type and arity from Alloy term:',AlloyTerm), | |
| 1539 | Type=[untyped], Arity=0. % like predicate | |
| 1540 | ||
| 1541 | % TO DO: maybe there are more primitive types? | |
| 1542 | % primitive types have arity zero in Alloy for some reason | |
| 1543 | is_primitive_type(['PrimitiveBoolean'],1). | |
| 1544 | ||
| 1545 | %atom_or_identifier_term(ID,ID) :- atom(ID). | |
| 1546 | %atom_or_identifier_term(identifier(IDName,_,_),IDName). | |
| 1547 | ||
| 1548 | join_predicates(Op,TArgList,TBinaryP) :- | |
| 1549 | alloy_to_b_operator(Op,BOp) , | |
| 1550 | (BOp = conjunct ; BOp = disjunct) , | |
| 1551 | join_untyped_ast_nodes(BOp,TArgList,TBinaryP). | |
| 1552 | ||
| 1553 | join_untyped_ast_nodes(_,[],truth(none)). | |
| 1554 | join_untyped_ast_nodes(BOp,[H|T],Conjoined) :- | |
| 1555 | join_untyped_ast_nodes(BOp,T,H,Conjoined). | |
| 1556 | ||
| 1557 | join_untyped_ast_nodes(_,[],Acc,Acc). | |
| 1558 | join_untyped_ast_nodes(BOp,[H|T],Acc,Conjoined) :- | |
| 1559 | NewAcc =.. [BOp,none,Acc,H], | |
| 1560 | join_untyped_ast_nodes(BOp,T,NewAcc,Conjoined). | |
| 1561 | ||
| 1562 | ||
| 1563 | :- begin_tests(full_machine_translation). | |
| 1564 | ||
| 1565 | test(cards,[]) :- | |
| 1566 | load_alloy_ast_prolog_file('../../prob_examples/public_examples/Alloy/Prolog/cards.pl'). | |
| 1567 | ||
| 1568 | test(filesystem,[]) :- | |
| 1569 | load_alloy_ast_prolog_file('../../prob_examples/public_examples/Alloy/Prolog/filesystem.pl'). | |
| 1570 | ||
| 1571 | test(filesystem2,[]) :- | |
| 1572 | load_alloy_ast_prolog_file('../../prob_examples/public_examples/Alloy/Prolog/filesystem2.pl'). | |
| 1573 | ||
| 1574 | test(self_grandpas,[]) :- | |
| 1575 | load_alloy_ast_prolog_file('../../prob_examples/public_examples/Alloy/Prolog/selfgrandpas.pl'). | |
| 1576 | ||
| 1577 | test(queens2,[]) :- | |
| 1578 | load_alloy_ast_prolog_file('../../prob_examples/public_examples/Alloy/Prolog/queens2.pl'). | |
| 1579 | ||
| 1580 | test(river_crossing,[]) :- | |
| 1581 | load_alloy_ast_prolog_file('../../prob_examples/public_examples/Alloy/Prolog/rivercrossingpuzzle.pl'). | |
| 1582 | ||
| 1583 | test(enum_test,[]) :- | |
| 1584 | load_alloy_ast_prolog_file('../../prob_examples/public_examples/Alloy/Prolog/enumtest.pl'). | |
| 1585 | ||
| 1586 | test(graphiso,[]) :- | |
| 1587 | load_alloy_ast_prolog_file('../../prob_examples/public_examples/Alloy/Prolog/graphiso.pl'). | |
| 1588 | ||
| 1589 | test(disj_field_test,[]) :- | |
| 1590 | load_alloy_ast_prolog_file('../../prob_examples/public_examples/Alloy/Prolog/disjfieldtest.pl'). | |
| 1591 | ||
| 1592 | test(crewAlloc,[]) :- | |
| 1593 | load_alloy_ast_prolog_file('../../prob_examples/public_examples/Alloy/Prolog/crewalloc.pl'). | |
| 1594 | ||
| 1595 | test(sudoku1,[]) :- | |
| 1596 | load_alloy_ast_prolog_file('../../prob_examples/public_examples/Alloy/Prolog/sudoku1.pl'). | |
| 1597 | ||
| 1598 | test(sequence_test,[]) :- | |
| 1599 | load_alloy_ast_prolog_file('../../prob_examples/public_examples/Alloy/Prolog/sequence_test.pl'). | |
| 1600 | ||
| 1601 | test(http,[]) :- | |
| 1602 | load_alloy_ast_prolog_file('../../prob_examples/public_examples/Alloy/Prolog/http.pl'). | |
| 1603 | ||
| 1604 | test(knights,[]) :- | |
| 1605 | load_alloy_ast_prolog_file('../../prob_examples/public_examples/Alloy/Prolog/knights_and_knaves.pl'). | |
| 1606 | ||
| 1607 | test(hanoi,[]) :- | |
| 1608 | load_alloy_ast_prolog_file('../../prob_examples/public_examples/Alloy/Prolog/hanoi.pl'). | |
| 1609 | ||
| 1610 | test(einstein,[]) :- | |
| 1611 | load_alloy_ast_prolog_file('../../prob_examples/public_examples/Alloy/Prolog/einstein.pl'). | |
| 1612 | ||
| 1613 | test(slot_data,[]) :- | |
| 1614 | load_alloy_ast_prolog_file('../../prob_examples/public_examples/Alloy/Prolog/slot_data_v2.pl'). | |
| 1615 | ||
| 1616 | test(job_puzzle,[]) :- | |
| 1617 | load_alloy_ast_prolog_file('../../prob_examples/public_examples/Alloy/Prolog/job_puzzle.pl'). | |
| 1618 | ||
| 1619 | /* | |
| 1620 | test(family_v1,[]) :- | |
| 1621 | load_alloy_ast_prolog_file('../../prob_examples/public_examples/Alloy/Prolog/family-v1.pl'). | |
| 1622 | ||
| 1623 | test(hanoi,[]) :- | |
| 1624 | load_alloy_ast_prolog_file('../../prob_examples/public_examples/Alloy/Prolog/hanoi.pl'). | |
| 1625 | ||
| 1626 | test(knights,[]) :- | |
| 1627 | load_alloy_ast_prolog_file('../../prob_examples/public_examples/Alloy/Prolog/knights_and_knaves.pl'). | |
| 1628 | ||
| 1629 | test(directctrl,[]) :- | |
| 1630 | load_alloy_ast_prolog_file('../../prob_examples/public_examples/Alloy/Prolog/directctrl.pl'). | |
| 1631 | ||
| 1632 | test(views,[]) :- | |
| 1633 | load_alloy_ast_prolog_file('../../prob_examples/public_examples/Alloy/Prolog/views.pl'). | |
| 1634 | ||
| 1635 | test(mutex,[]) :- | |
| 1636 | load_alloy_ast_prolog_file('../../prob_examples/public_examples/Alloy/Prolog/mutex.pl'). | |
| 1637 | */ | |
| 1638 | :- end_tests(full_machine_translation). |