| 1 | % (c) 2017-2024 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 | :- module(alloy2b, [load_alloy_ast_prolog_file/1, | |
| 5 | load_alloy_model/2, | |
| 6 | load_alloy_model/3, | |
| 7 | translate_alloy_model/3, | |
| 8 | get_command_names/1, | |
| 9 | get_skipped_command_names/1, | |
| 10 | get_translated_command_names/1, | |
| 11 | load_command_in_current_translation/1]). | |
| 12 | ||
| 13 | :- meta_predicate map_translate(3, -, -, -). | |
| 14 | ||
| 15 | :- use_module(library(lists)). | |
| 16 | :- use_module(library(file_systems)). | |
| 17 | :- use_module(library(sets), [subtract/3]). | |
| 18 | :- use_module(library(aggregate),[forall/2]). | |
| 19 | :- use_module(probsrc(debug)). | |
| 20 | :- use_module(probsrc(bmachine)). | |
| 21 | :- use_module(probsrc(translate)). | |
| 22 | :- use_module(probsrc(preferences), [get_preference/2,temporary_set_preference/2]). | |
| 23 | :- use_module(probsrc(error_manager)). | |
| 24 | :- use_module(probsrc(bmachine)). | |
| 25 | :- use_module(probsrc(bsyntaxtree)). | |
| 26 | :- use_module(probsrc(specfile), [set_animation_minor_mode/1]). | |
| 27 | :- use_module(probsrc(tools_strings), [atom_prefix/2, atom_suffix/2, ajoin/2]). | |
| 28 | :- use_module(probsrc(tools_positions), [row_col_to_position/3, is_valid_position/1]). | |
| 29 | ||
| 30 | :- set_prolog_flag(double_quotes, codes). | |
| 31 | ||
| 32 | :- dynamic natural_type/1, integer_type/1, sig_field_id/2, enumerated_set/1, singleton_set/1, total_function/2, | |
| 33 | ordered_signature/1, extending_signatures/1, is_sub_signature_of/3, is_seq/1, | |
| 34 | maxseq/1, artificial_parent_type/3, abstract_sig/1, definition_without_param/1, | |
| 35 | skipped_command/2, translated_command/2, model_path/1, fact/1, assertion/1. | |
| 36 | :- volatile natural_type/1, integer_type/1, sig_field_id/2, enumerated_set/1, singleton_set/1, total_function/2, | |
| 37 | ordered_signature/1, extending_signatures/1, is_sub_signature_of/3, is_seq/1, | |
| 38 | maxseq/1, artificial_parent_type/3, abstract_sig/1, definition_without_param/1, | |
| 39 | skipped_command/2, translated_command/2, model_path/1, fact/1, assertion/1. | |
| 40 | ||
| 41 | default_upper_bound_scope(3). | |
| 42 | default_max_seq(7). | |
| 43 | set_max_seq(Max) :- number(Max), Max \== -1, !, assertz(maxseq(Max)). | |
| 44 | set_max_seq(_) :- default_max_seq(D), assertz(maxseq(D)). | |
| 45 | ||
| 46 | % An automated translation from Alloy to classical B. | |
| 47 | % The Alloy abstract syntax tree is translated to an untyped B AST as supported by ProB. | |
| 48 | % Afterwards, the untyped AST can be typechecked and loaded by ProB. | |
| 49 | % The used positions are from the Alloy parser and thus refer to the Alloy model. | |
| 50 | % Usage: | |
| 51 | % 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 | |
| 52 | % translate_alloy_model/3: input is an Alloy model represented as a Prolog term as provided by the Kotlin translation, output is an untyped B AST | |
| 53 | % Run tests: | |
| 54 | % - launch ProB Tcl/Tk or ProB CLI | |
| 55 | % - 'use_module(probsrc('alloy2b/alloy2b')).' | |
| 56 | % - 'error_manager:reset_errors , plunit:run_tests(full_machine_translation).'. | |
| 57 | % - run a single test: 'error_manager:reset_errors , plunit:run_tests(full_machine_translation:directctrl).' | |
| 58 | % - 'bmachine:full_b_machine(L) , translate:print_machine(L)'. | |
| 59 | % Further tests are integrated in testsrc(testcases). | |
| 60 | % | |
| 61 | % KNOWN ISSUES / TO DOs | |
| 62 | % ---------------------- | |
| 63 | % - nested quantifiers: the usage of facts for singleton_set is error prone, and cannot deal with | |
| 64 | % nested quantifiers with variable clashes, in particular when in the inner quantifier the | |
| 65 | % identifier is not a singleton set | |
| 66 | % - nested multiplicity annotations for non-binary relations (Joshua: is this possible in Alloy?) | |
| 67 | % - variable capture due to use of DEFINITIONS | |
| 68 | % - modulo currently only works for positive numbers | |
| 69 | ||
| 70 | load_alloy_ast_prolog_file(File) :- | |
| 71 | \+ file_exists(File, read), | |
| 72 | !, | |
| 73 | add_error(load_alloy_ast_prolog_file, 'Alloy AST file has not been created:', [File]), | |
| 74 | fail. | |
| 75 | load_alloy_ast_prolog_file(File) :- | |
| 76 | load_alloy_ast_prolog_file_for_command(_, File). | |
| 77 | ||
| 78 | %% load_alloy_ast_prolog_file_for_command(?CmdName, +File). | |
| 79 | % First command is chosen as main command if CmdName is a variable. | |
| 80 | load_alloy_ast_prolog_file_for_command(CmdName, File) :- | |
| 81 | formatsilent('Opening Alloy AST file: ~w~n', [File]), | |
| 82 | open(File, read, Stream), | |
| 83 | safe_read_term(Stream, AlloyTerm), | |
| 84 | close(Stream), | |
| 85 | retractall(model_path(_)), | |
| 86 | asserta(model_path(File)), | |
| 87 | load_alloy_model(CmdName, AlloyTerm, 'alloytranslation'). | |
| 88 | ||
| 89 | %% load_command_in_current_translation(+CmdName). | |
| 90 | % If the selected command is currently not translated, reload the machine and translate the command. | |
| 91 | % Otherwise, there is nothing to do. | |
| 92 | % Note that we do not translate commands with different scopes at once. | |
| 93 | load_command_in_current_translation(CmdName) :- | |
| 94 | ( skipped_command(_, CmdName) | |
| 95 | -> model_path(File), | |
| 96 | load_alloy_ast_prolog_file_for_command(CmdName, File) | |
| 97 | ; true | |
| 98 | ). | |
| 99 | ||
| 100 | safe_read_term(Stream, Term) :- | |
| 101 | catch(read(Stream, Term), error(E,_), ( | |
| 102 | add_internal_error('Exception while reading Prolog term from stream:', E), | |
| 103 | fail | |
| 104 | )). | |
| 105 | ||
| 106 | assert_integer_type_from_preference :- | |
| 107 | get_preference(alloy_use_implementable_integers, Pref), | |
| 108 | retractall(integer_type(_)), | |
| 109 | retractall(natural_type(_)), | |
| 110 | ( Pref == true | |
| 111 | -> asserta(integer_type('INT')), | |
| 112 | asserta(natural_type('NAT')) | |
| 113 | ; asserta(integer_type('INTEGER')), | |
| 114 | asserta(natural_type('NATURAL')) | |
| 115 | ). | |
| 116 | ||
| 117 | % TO DO: fix translation of Marc's machines | |
| 118 | ||
| 119 | % TO DO: do we need to translate the 'expect' keyword for commands? is it inlined by the alloy parser? | |
| 120 | ||
| 121 | load_alloy_model(AlloyTerm, AlloyFile) :- | |
| 122 | % use the first run or check command by default for models that use sequences, otherwise all commands are translated | |
| 123 | load_alloy_model(_FirstRunOrCheck, AlloyTerm, AlloyFile). | |
| 124 | ||
| 125 | load_alloy_model(CurrentCommand, AlloyTerm, AlloyFile) :- | |
| 126 | assert_integer_type_from_preference, | |
| 127 | reset_errors, | |
| 128 | debug_format(19, 'Translating AST to B.~n', []), | |
| 129 | retract_state, | |
| 130 | % tools_printing:nested_print_term(AlloyTerm,10), | |
| 131 | translate_alloy_model(CurrentCommand, AlloyTerm, UntypedBAst), | |
| 132 | !, | |
| 133 | UntypedBAst = machine(generated(none,AbstractMachine)), % like @generated pragma | |
| 134 | set_animation_minor_mode(alloy), | |
| 135 | b_load_machine_from_term(AlloyFile, complete_machine('alloytranslation',[AbstractMachine],[AlloyFile])). | |
| 136 | load_alloy_model(CurrentCommand, _, _) :- | |
| 137 | \+ integer(CurrentCommand), | |
| 138 | add_error(load_alloy_model, 'Current command has to be an integer:', CurrentCommand), | |
| 139 | fail. | |
| 140 | load_alloy_model(_, AlloyTerm, _) :- | |
| 141 | add_error(load_alloy_model, 'Translating Alloy AST failed:', AlloyTerm), | |
| 142 | fail. | |
| 143 | ||
| 144 | process_options(Options) :- | |
| 145 | ( \+member(sequences:_, Options) | |
| 146 | ; \+member(parent_types:_, Options) | |
| 147 | ), | |
| 148 | !, | |
| 149 | add_error(alloy2b, 'Alloy2B parser failed to analyze types or check for sequences (be sure Alloy2B parser library is up-to-date).',[]), | |
| 150 | fail. | |
| 151 | process_options(Options) :- | |
| 152 | process_options_safe(Options). | |
| 153 | ||
| 154 | process_options_safe(Options) :- | |
| 155 | select(parent_types:SetOfTypeSets, Options, RestOptions), | |
| 156 | !, | |
| 157 | assert_artificial_parent_types(SetOfTypeSets), | |
| 158 | process_options_safe(RestOptions). | |
| 159 | process_options_safe(_). | |
| 160 | ||
| 161 | % Given a list of list of signature names. We need to introduce a parent type in B for each list of signatures. | |
| 162 | assert_artificial_parent_types(SetOfTypeSets) :- | |
| 163 | assert_artificial_parent_types(0, SetOfTypeSets). | |
| 164 | ||
| 165 | assert_artificial_parent_types(_, []). | |
| 166 | assert_artificial_parent_types(C, [SetOfTypes|T]) :- | |
| 167 | gen_identifier(C, "_universe", ParentId), | |
| 168 | gen_identifier(C, "_Universe", PParentId), | |
| 169 | C1 is C + 1, | |
| 170 | assert_parent_id_for_types(SetOfTypes, ParentId, PParentId), | |
| 171 | assert_artificial_parent_types(C1, T). | |
| 172 | ||
| 173 | assert_parent_id_for_types([], _, _). | |
| 174 | assert_parent_id_for_types([SignatureName|T], ParentId, PParentId) :- | |
| 175 | asserta(artificial_parent_type(SignatureName,ParentId,PParentId)), | |
| 176 | assert_parent_id_for_types(T, ParentId, PParentId). | |
| 177 | ||
| 178 | % Log the current module to define unique field names. | |
| 179 | :- dynamic module_in_scope_but_root/2, current_module_in_scope/1. | |
| 180 | :- volatile module_in_scope_but_root/2, current_module_in_scope/1. | |
| 181 | ||
| 182 | % Translate an Alloy model and all its imports (excluding some utility libraries we provide manual implementations for). | |
| 183 | translate_alloy_model(CurrentCommand, alloy(RootModule,Models), UntypedBAst) :- | |
| 184 | retractall(translate:atelierb_mode(_)), | |
| 185 | select(alloy_model((RootModule,Alias),Facts,Assertions,Commands,Functions,Sigs,OSigNames,Opts), Models, RestModels), | |
| 186 | !, | |
| 187 | catch( | |
| 188 | translate_alloy_models(CurrentCommand, alloy_model((RootModule,Alias),Facts,Assertions,Commands,Functions,Sigs,OSigNames,Opts), RestModels, UntypedBAst), | |
| 189 | Exc, | |
| 190 | (add_internal_error('Exception while translating Alloy model:',Exc),fail)). | |
| 191 | ||
| 192 | translate_alloy_models(CurrentCommand, alloy_model((RootModule,RootAlias),Facts,Assertions,Commands,Functions,Signatures,OSigNames,Options), RestModels, UntypedBAst) :- | |
| 193 | empty_machine_acc(MAcc), | |
| 194 | forall( | |
| 195 | member(alloy_model((ModuleName,Alias),_,_,_,_,_,_,_),RestModels), | |
| 196 | asserta(module_in_scope_but_root(ModuleName,Alias)) | |
| 197 | ), | |
| 198 | ( ground(CurrentCommand) | |
| 199 | -> NOptions = [is_root_module,translate_command:CurrentCommand|Options] | |
| 200 | ; NOptions = [is_root_module|Options] | |
| 201 | ), | |
| 202 | translate_alloy_models_acc(MAcc, | |
| 203 | alloy_model((RootModule,RootAlias),Facts,Assertions,Commands,Functions,Signatures,OSigNames,NOptions), | |
| 204 | RestModels, UntypedBAst). | |
| 205 | ||
| 206 | translate_alloy_models_acc(MAcc, AlloyModel, RestModels, UntypedBAst) :- | |
| 207 | translate_single_alloy_model(AlloyModel, MAcc, NewMAcc), | |
| 208 | ( RestModels == [] | |
| 209 | -> debug_println(19, build_machine_ast), | |
| 210 | build_machine_ast(NewMAcc, UntypedBAst), | |
| 211 | assert_atelierb_mode, | |
| 212 | % tools_printing:nested_print_term(UntypedBAst,20), | |
| 213 | ( debug_mode(off) -> true | |
| 214 | ; nl, | |
| 215 | ( translate:print_raw_machine_terms(UntypedBAst) | |
| 216 | ; debug_println(19, 'translate:print_raw_machine_terms/1 failed.')), | |
| 217 | nl | |
| 218 | ), ! | |
| 219 | ; RestModels = [ImportedModel|T], | |
| 220 | translate_alloy_models_acc(NewMAcc, ImportedModel, T, UntypedBAst)). | |
| 221 | ||
| 222 | skip_module(ModuleName) :- | |
| 223 | supported_default_module(ModuleName); unsupported_module(ModuleName). | |
| 224 | ||
| 225 | assert_atelierb_mode :- | |
| 226 | get_preference(alloy_translation_for_proof, true), | |
| 227 | !, | |
| 228 | temporary_set_preference(translate_print_typing_infos, true), | |
| 229 | translate:set_atelierb_mode(native). | |
| 230 | assert_atelierb_mode. | |
| 231 | ||
| 232 | % Alloy utility modules we provide manual implementations for. | |
| 233 | supported_default_module('util''boolean'). | |
| 234 | supported_default_module('util''integer'). | |
| 235 | supported_default_module('util''natural'). | |
| 236 | supported_default_module('util''ordering'). | |
| 237 | supported_default_module('util''relation'). | |
| 238 | supported_default_module('util''sequence'). | |
| 239 | ||
| 240 | unsupported_module('util''sequniv'). % uses univ type in function args; we probably do not need this module as it provides the same functions as util/sequence | |
| 241 | unsupported_module('util''seqrel'). % TO DO: ? | |
| 242 | unsupported_module('util''time'). % TO DO: ? | |
| 243 | % following modules are translated using the tool: util/graph, util/ternary | |
| 244 | ||
| 245 | % Give unique names for identifiers of imported modules (prepend module name). | |
| 246 | % Identifier names in the root module are not extended. | |
| 247 | assert_current_module_in_scope(ModuleName, Alias) :- | |
| 248 | module_in_scope_but_root(ModuleName, Alias), | |
| 249 | retractall(current_module_in_scope(_)), | |
| 250 | asserta(current_module_in_scope(ModuleName)). | |
| 251 | assert_current_module_in_scope(_, _). | |
| 252 | ||
| 253 | option_defines_cmd_for_root(Options, CmdName) :- | |
| 254 | member(is_root_module, Options), | |
| 255 | member(translate_command:CmdName, Options). | |
| 256 | ||
| 257 | get_command_by_name(Commands, CmdName, MainCommand, CommandId, RestCommands) :- | |
| 258 | get_command_by_name(Commands, CmdName, 0, 0, MainCommand, CommandId, [], RestCommands). | |
| 259 | ||
| 260 | get_command_by_name([Command|T], CmdName, Run, Check, MainCommand, CommandId, AccRest, RestCommands) :- | |
| 261 | functor(Command, Functor, _), | |
| 262 | ( Functor == check | |
| 263 | -> NewCheck is Check + 1, | |
| 264 | NewRun = Run, | |
| 265 | TempId = Check | |
| 266 | ; NewRun is Run + 1, | |
| 267 | NewCheck = Check, | |
| 268 | TempId = Run | |
| 269 | ), | |
| 270 | number_codes(TempId, CTempId), | |
| 271 | atom_codes(ATempId, CTempId), | |
| 272 | atom_concat(Functor, ATempId, TempCmdName), | |
| 273 | ( CmdName == TempCmdName | |
| 274 | -> MainCommand = Command, | |
| 275 | CommandId = TempId, | |
| 276 | append(AccRest, T, RestCommands) | |
| 277 | ; append(AccRest, [Command], NAccRest), % append to keep order | |
| 278 | get_command_by_name(T, CmdName, NewRun, NewCheck, MainCommand, CommandId, NAccRest, RestCommands) | |
| 279 | ). | |
| 280 | ||
| 281 | ||
| 282 | translate_single_alloy_model(alloy_model((ModuleName,_),_,_,_,_,_,_,_), MAcc, MAcc) :- | |
| 283 | skip_module(ModuleName), | |
| 284 | !. | |
| 285 | translate_single_alloy_model(alloy_model((ModuleName,Alias),facts(Facts),assertions(Assertions),commands(Commands),functions(Functions), | |
| 286 | signatures(Signatures),ordered_signatures(OSigNames),Options), MAcc, NewMAcc) :- | |
| 287 | % singleton sets are asserted at runtime using singleton_set/1 | |
| 288 | % accumulate all translations, afterwards we build the untyped machine ast | |
| 289 | assert_current_module_in_scope(ModuleName, Alias), | |
| 290 | process_options(Options), | |
| 291 | maplist(assert_ordered_sig_name, OSigNames), | |
| 292 | ( option_defines_cmd_for_root(Options, CmdName) | |
| 293 | -> % a specific command id is set to be translated | |
| 294 | get_command_by_name(Commands, CmdName, MainCommand, CommandId, _RestCommands) | |
| 295 | ; % select the first command to be translated | |
| 296 | ( Commands = [MainCommand|_RestCommands] | |
| 297 | -> CommandId = 0 | |
| 298 | ; add_internal_error('Could not find main command id: ',CommandId) | |
| 299 | ) | |
| 300 | ), | |
| 301 | % assertions and facts are inlined in run or check commands and not translated in the properties | |
| 302 | length(Commands,NrOfCommands), | |
| 303 | get_command_scopes(MainCommand, GS, ExactScopes, UpBoundScopes, BitWidth, CmdMaxSeq), | |
| 304 | formatsilent('Scopes for main command ~w (~w commands) : global=~w, exact=~w, bw=~w, maxseq=~w~n', | |
| 305 | [CommandId,NrOfCommands,GS,ExactScopes,BitWidth,CmdMaxSeq]), | |
| 306 | set_max_seq(CmdMaxSeq), % we need max seq scope for signature fields | |
| 307 | !, | |
| 308 | ||
| 309 | debug_println(19, translating_signatures), | |
| 310 | maplist(preprocess_signature, Signatures), % assertz some signature names as singleton | |
| 311 | ||
| 312 | define_artificial_parent_types_if_necessary(MAcc, MAcc1, GS, ExactScopes, UpBoundScopes), | |
| 313 | map_translate(translate_signature, MAcc1, Signatures, MAcc2), | |
| 314 | ||
| 315 | ( number(GS), GS > 0 | |
| 316 | -> preferences:temporary_set_preference(globalsets_fdrange, GS) % TO DO: improve | |
| 317 | ; true | |
| 318 | ), | |
| 319 | ( get_preference(alloy_scopeless_translation,true) % do not set any scopes (useful for proof assistants) | |
| 320 | -> MAcc3 = MAcc2 | |
| 321 | ; try_set_bitwidth(BitWidth), | |
| 322 | get_signature_names_from_machine_acc(MAcc2, SignatureNames), | |
| 323 | translate_scopes_for_command(MainCommand,SignatureNames,ScopePreds), | |
| 324 | extend_machine_with_conjuncts(properties, [ScopePreds], MAcc2, MAcc3) | |
| 325 | ), | |
| 326 | debug_println(19, translating_functions), | |
| 327 | map_translate(translate_function, MAcc3, Functions, MAcc4), | |
| 328 | debug_println(19, translating_facts), | |
| 329 | map_translate(translate_fact, MAcc4, Facts, MAcc5), | |
| 330 | debug_println(19, translating_assertions), | |
| 331 | map_translate(translate_assertion, MAcc5, Assertions, MAcc6), | |
| 332 | debug_println(19, translating_commands), | |
| 333 | translate_commands(CommandId, MainCommand, MAcc6, Commands, MAcc7), | |
| 334 | !, | |
| 335 | finalize_extending_signatures(MAcc7, NewMAcc). | |
| 336 | ||
| 337 | get_command_name(CmdFunctor, ID, CmdName) :- | |
| 338 | number_codes(ID, Codes), | |
| 339 | atom_codes(AID, Codes), | |
| 340 | atom_concat(CmdFunctor, AID, CmdName). | |
| 341 | ||
| 342 | calculate_max_parent_type_card(SigNames, GlobalScope, ExactScopes, UpBoundScopes, MaxCard) :- | |
| 343 | calculate_max_parent_type_card(SigNames, GlobalScope, ExactScopes, UpBoundScopes, 0, MaxCard). | |
| 344 | ||
| 345 | calculate_max_parent_type_card([], _, _, _, Acc, Acc). | |
| 346 | calculate_max_parent_type_card([SigName|T], GlobalScope, ExactScopes, UpBoundScopes, Acc, MaxCard) :- | |
| 347 | ( (member((SigName,Scope), ExactScopes); member((SigName,Scope), UpBoundScopes)) | |
| 348 | -> NAcc is Acc + Scope | |
| 349 | ; NAcc is Acc + GlobalScope | |
| 350 | ), | |
| 351 | calculate_max_parent_type_card(T, GlobalScope, ExactScopes, UpBoundScopes, NAcc, MaxCard). | |
| 352 | ||
| 353 | % Introduce parent types in B for Alloy signatures without a common parent type but univ that interact with each other. | |
| 354 | define_artificial_parent_types_if_necessary(MAcc, NewMAcc, GlobalScope, ExactScopes, UpBoundScopes) :- | |
| 355 | findall((ParentId,PParentId), artificial_parent_type(_, ParentId, PParentId), TParents), | |
| 356 | remove_dups(TParents, Parents), | |
| 357 | define_artificial_parent_types(MAcc, Parents, NewMAcc, GlobalScope, ExactScopes, UpBoundScopes). | |
| 358 | ||
| 359 | define_artificial_parent_types(MAcc, [], MAcc, _, _, _). | |
| 360 | define_artificial_parent_types(MAcc, [(ParentId,PParentId)|T], NewMAcc, GlobalScope, ExactScopes, UpBoundScopes) :- | |
| 361 | PParentId = identifier(_,PParentName), | |
| 362 | findall(SigName, artificial_parent_type(SigName,ParentId,_), DSigNames), | |
| 363 | DSigNames \== [], | |
| 364 | remove_dups(DSigNames, SigNames), | |
| 365 | maplist(translate_e_p, SigNames, TSigNames), | |
| 366 | % should be: _universe0 = S1 \/ .. \/ Sn | |
| 367 | % ProB currently does not set the deferred set size of P0 in cbc mode if it is defined within an operation's precondition | |
| 368 | % (ProB uses the preference 'deferred_setsize' which then might be a contradiction) | |
| 369 | % this equality is valid if it is translated in the properties and not as a precondition which is the case | |
| 370 | % if we only translate a single run or check command | |
| 371 | % _universe0 = S1 \/ .. \/ Sn | |
| 372 | join_untyped_ast_nodes(union, TSigNames, Union), | |
| 373 | ParentDomain = equal(none,ParentId,Union), | |
| 374 | % TO DO: use above code if this issue is solved, otherwise stick to this translation which is just less performant in case we do not constrain _P0 | |
| 375 | % if we constrain _P0, e.g., using id(_P0), this could be an error as _P0 possibly contains more elements than necessary | |
| 376 | % Note: if preference 'deferred_setsize' is smaller than n, this is still a contradiction | |
| 377 | % S1 \/ .. \/ Sn <: universe0 | |
| 378 | %join_untyped_ast_nodes(union, TSigNames, Union), | |
| 379 | %ParentDomain = subset(none, Union, ParentId), | |
| 380 | extend_machine_acc(properties, MAcc, ParentDomain, MAcc1), | |
| 381 | calculate_max_parent_type_card(SigNames, GlobalScope, ExactScopes, UpBoundScopes, MaxCard), | |
| 382 | % _universe0 <: _Universe0 & card(_Universe0) = MaxCard | |
| 383 | Subset = subset(none,ParentId,PParentId), | |
| 384 | CardEq = equal(none,card(none,PParentId),integer(none,MaxCard)), | |
| 385 | extend_machine_acc(properties, MAcc1, conjunct(none,Subset,CardEq), MAcc2), | |
| 386 | % S1 /\ S2 = {} & .. & Sn-1 /\ Sn = {} | |
| 387 | disjoint_set_of_signatures(TSigNames, DisjointConstraint), | |
| 388 | extend_machine_acc(properties, MAcc2, DisjointConstraint, MAcc3), | |
| 389 | extend_machine_acc(constants, MAcc3, ParentId, MAcc4), | |
| 390 | extend_machine_acc(sets, MAcc4, deferred_set(none,PParentName), MAcc5), | |
| 391 | define_artificial_parent_types(MAcc5, T, NewMAcc, GlobalScope, ExactScopes, UpBoundScopes). | |
| 392 | ||
| 393 | disjoint_set_of_signatures(TSigNames, DisjointConstraint) :- | |
| 394 | get_signature_pairs(TSigNames, SigPairs), | |
| 395 | disjoint_set_of_signatures_from_pairs(SigPairs, [], DisjointList), | |
| 396 | join_untyped_ast_nodes(conjunct, DisjointList, DisjointConstraint). | |
| 397 | ||
| 398 | disjoint_set_of_signatures_from_pairs([], Acc, Acc). | |
| 399 | disjoint_set_of_signatures_from_pairs([(S1,S2)|T], Acc, DisjointList) :- | |
| 400 | Disjoint = equal(none,intersection(none,S1,S2),empty_set(none)), | |
| 401 | disjoint_set_of_signatures_from_pairs(T, [Disjoint|Acc], DisjointList). | |
| 402 | ||
| 403 | get_signature_pairs(TSigNames, SigPairs) :- | |
| 404 | findall((S1,S2), (nth0(I1, TSigNames, S1), nth0(I2, TSigNames, S2), I1 < I2), SigPairs). | |
| 405 | ||
| 406 | ||
| 407 | map_translate(_, MAcc, [], MAcc). | |
| 408 | map_translate(TypePred, MAcc, [Part|T], Res) :- | |
| 409 | call(TypePred, MAcc, Part, NewMAcc), | |
| 410 | map_translate(TypePred, NewMAcc, T, Res). | |
| 411 | ||
| 412 | try_set_bitwidth(BitWidth) :- | |
| 413 | BitWidth = bitwidth(BW), | |
| 414 | number(BW), | |
| 415 | BW > 0, | |
| 416 | !, | |
| 417 | MaxInt is truncate(2**(BW-1))-1, | |
| 418 | MinInt is truncate(-(2**(BW-1))), | |
| 419 | preferences:temporary_set_preference(maxint, MaxInt), | |
| 420 | preferences:temporary_set_preference(minint, MinInt). | |
| 421 | try_set_bitwidth(_). | |
| 422 | ||
| 423 | % things that need to be done before translating the signatures, e.g., assertz singleton set info | |
| 424 | preprocess_signature(signature(Name,_Fields,_Facts,Options,_)) :- | |
| 425 | % assertz signatures for singleton checks | |
| 426 | assert_singleton_set(Options, Name), | |
| 427 | assert_abstract_sig(Options, Name), | |
| 428 | assert_enumerated_set(Options, Name). | |
| 429 | ||
| 430 | % translate signature declaration sig Name {Fields} | |
| 431 | translate_signature(MAcc, signature(Name,Fields,Facts,Options,pos(Col,Row)), NewMAcc) :- | |
| 432 | extend_machine_acc(signatures, MAcc, [Name], MAcc1), | |
| 433 | translate_signature_aux(Name, Options, pos(Col,Row), MAcc1, MAcc2), | |
| 434 | translate_signature_fields(Fields, Name, MAcc2, MAcc3), | |
| 435 | translate_e_p(Name, TName), | |
| 436 | map_translate(translate_signature_fact(TName), MAcc3, Facts, NewMAcc). | |
| 437 | ||
| 438 | translate_signature_aux(Name, Options, Pos, MAcc, NewMAcc) :- | |
| 439 | % ordered signatures are defined as distinct sets of integer when translating a command | |
| 440 | member(ordered, Options), | |
| 441 | !, | |
| 442 | define_ordered_signature_functions(Pos, MAcc, Name, MAcc1), | |
| 443 | extend_machine_acc(signatures, MAcc1, [Name], MAcc2), | |
| 444 | translate_e_p(Name, TID), | |
| 445 | integer_type(IntOrInteger), | |
| 446 | formatsilent('Ordered signature = ~w~n',[Name]), | |
| 447 | extend_machine_acc(properties, MAcc2, | |
| 448 | member(none,TID,pow_subset(none,integer_set(none,IntOrInteger))), MAcc3), | |
| 449 | define_sig_as_set_or_constant_aux(constants, MAcc3, Name, Options, Pos, NewMAcc). | |
| 450 | translate_signature_aux(Name, Options, Pos, MAcc, NewMAcc) :- | |
| 451 | define_sig_as_set_or_constant(MAcc, Name, Options, Pos, NewMAcc). | |
| 452 | ||
| 453 | define_ordered_signature_functions(POS, MAcc, Sig, NewMAcc) :- | |
| 454 | translate_pos(POS, BPOS), | |
| 455 | gen_identifier(0, "_c_", TIDX), | |
| 456 | TIDS = identifier(BPOS,s), | |
| 457 | translate_e_p(Sig, TSig), | |
| 458 | MemberX = member(BPOS,TIDX,TSig), | |
| 459 | % next_Sig(s) == IF succ[s] <: Sig THEN succ[s] ELSE {} END | |
| 460 | atom_concat(next_, Sig, NextName), | |
| 461 | SuccessorImg = image(BPOS,successor(BPOS),TIDS), | |
| 462 | PredecessorImg = image(BPOS,predecessor(BPOS),TIDS), | |
| 463 | extend_machine_acc(definitions, MAcc, | |
| 464 | expression_definition(BPOS,NextName,[TIDS],if_then_else(BPOS,subset(BPOS,SuccessorImg,TSig),SuccessorImg,empty_set(BPOS))), MAcc1), | |
| 465 | % nexts_Sig(s) == {x|x:Sig & min({x} \/ s) /= x} | |
| 466 | atom_concat(nexts_, Sig, NextsName), | |
| 467 | NextsBody = conjunct(BPOS,MemberX,not_equal(BPOS,min(BPOS,union(BPOS,set_extension(BPOS,[TIDX]),TIDS)),TIDX)), | |
| 468 | extend_machine_acc(definitions, MAcc1, | |
| 469 | expression_definition(BPOS,NextsName,[TIDS],comprehension_set(BPOS,[TIDX],NextsBody)), MAcc2), | |
| 470 | atom_concat(prev_, Sig, PrevName), | |
| 471 | % prev_Sig(s) == IF pred[s] <: Sig THEN pred[s] ELSE {} END | |
| 472 | extend_machine_acc(definitions, MAcc2, | |
| 473 | expression_definition(BPOS,PrevName,[TIDS],if_then_else(BPOS,subset(BPOS,PredecessorImg,TSig),PredecessorImg,empty_set(BPOS))), MAcc3), | |
| 474 | % prevs_Sig(s) == {x|x:Sig & max({x} \/ s) /= x} | |
| 475 | atom_concat(prevs_, Sig, PrevsName), | |
| 476 | PrevsBody = conjunct(BPOS,MemberX,not_equal(BPOS,max(BPOS,union(BPOS,set_extension(BPOS,[TIDX]),TIDS)),TIDX)), | |
| 477 | extend_machine_acc(definitions, MAcc3, | |
| 478 | expression_definition(BPOS,PrevsName,[TIDS],comprehension_set(BPOS,[TIDX],PrevsBody)), NewMAcc). | |
| 479 | ||
| 480 | translate_signature_fields(Fields, SignatureName) --> | |
| 481 | { translate_e_p(SignatureName, TSignatureName) }, | |
| 482 | translate_signature_fields_aux(Fields, SignatureName, TSignatureName). | |
| 483 | ||
| 484 | translate_signature_fields_aux([], _, _) --> | |
| 485 | []. | |
| 486 | translate_signature_fields_aux([Field|T], SignatureName, TSignatureName) --> | |
| 487 | translate_signature_field(SignatureName, TSignatureName, Field), | |
| 488 | translate_signature_fields_aux(T, SignatureName, TSignatureName). | |
| 489 | ||
| 490 | translate_signature_field(SignatureName, TSignatureName, Field, MAcc, NewMAcc) :- | |
| 491 | translate_signature_field_aux(SignatureName, TSignatureName, Field, TField, MAcc, MAcc1), | |
| 492 | extend_machine_acc(properties, MAcc1, TField, NewMAcc). | |
| 493 | ||
| 494 | translate_signature_field_aux(SignatureName, TSignatureName, | |
| 495 | field(FieldID,Expr,_FieldType,Options,POS), TFieldPred, MAcc, NewMAcc) :- | |
| 496 | FieldID = identifier(FieldName,_,_), | |
| 497 | asserta(sig_field_id(FieldName, SignatureName)), | |
| 498 | translate_e_p(FieldID, TFieldID), | |
| 499 | extend_machine_acc(constants, MAcc, TFieldID, MAcc1), | |
| 500 | translate_pos(POS, BPOS), | |
| 501 | disjoint_field_declaration(TSignatureName, BPOS, Options, MAcc1, TFieldID, NewMAcc), | |
| 502 | translate_field_decl(BPOS, SignatureName, TSignatureName, Expr, FieldID, TFieldID, TFieldPred), | |
| 503 | !. | |
| 504 | ||
| 505 | translate_function_field(field(FieldName,Expr,type(_Type,_Arity),_Options,POS), TField) :- | |
| 506 | % (Functor = function -> assert_singleton_set(FieldName) ; true) , % NO LONGER NEEDED | |
| 507 | translate_e_p(FieldName, TTFieldName), | |
| 508 | strip_singleton_set_from_this(TTFieldName, TFieldName), % necessary for nested definition calls with 'this' | |
| 509 | translate_pos(POS, BPOS), | |
| 510 | fun_or_pred_decl_special_cases(Expr, TFieldName, BPOS, TField, _IsSingleton), | |
| 511 | !. | |
| 512 | % TO DO: !! what if IsSingleton is set !! | |
| 513 | disjoint_field_declaration(TSignatureName, TPos, Options, MAcc, TFieldName, NewMAcc) :- | |
| 514 | member(disj, Options), | |
| 515 | !, | |
| 516 | % all a, b: S | a != b implies no a.f & b.f | |
| 517 | IdA = identifier(TPos,a), | |
| 518 | IdB = identifier(TPos,b), | |
| 519 | ImplLhs = conjunct(TPos,conjunct(TPos,member(TPos,IdA,TSignatureName),member(TPos,IdB,TSignatureName)), | |
| 520 | not_equal(TPos,IdA,IdB)), | |
| 521 | ImplRhs = equal(TPos,intersection(TPos,image(TPos,TFieldName,set_extension(none,[IdA])), | |
| 522 | image(TPos,TFieldName,set_extension(none,[IdB]))),empty_set(TPos)), | |
| 523 | Disjoint = forall(TPos,[IdA,IdB],implication(TPos,ImplLhs,ImplRhs)), | |
| 524 | extend_machine_acc(properties, MAcc, Disjoint, NewMAcc). | |
| 525 | disjoint_field_declaration(_, _, _, MAcc, _, MAcc). | |
| 526 | ||
| 527 | ||
| 528 | is_disjoint_quantifier(Fields) :- | |
| 529 | Fields = [F|_], | |
| 530 | is_disjoint_quantifier_field(F). % assumption: all or no field is disjoint | |
| 531 | is_disjoint_quantifier_field(field(_FieldName,_Expr,type(_Type,_Arity),Options,_POS)) :- | |
| 532 | member(disj, Options). | |
| 533 | ||
| 534 | translate_quantifier_field(field(FieldName,Expr,Type,_Options,POS), TField, NName) :- | |
| 535 | translate_pos(POS, BPOS), | |
| 536 | fun_or_pred_decl_special_cases(Expr, TFieldName, BPOS, TField, IsSingleton), | |
| 537 | !, | |
| 538 | ( IsSingleton == singleton | |
| 539 | -> FieldName = identifier(Name,_,_), | |
| 540 | prepend_identifier_of_module_import(Name, Type, NName), | |
| 541 | assert_singleton_set(NName) | |
| 542 | ; NName = alloy2b_none | |
| 543 | ), | |
| 544 | translate_e_p(FieldName, TFieldName). | |
| 545 | ||
| 546 | translate_fact(MAcc, fact(Expr,_Pos), NewMAcc) :- | |
| 547 | translate_e_p(Expr, TExpr), | |
| 548 | asserta(fact(Expr)), | |
| 549 | extend_machine_acc(properties, MAcc, TExpr, NewMAcc). | |
| 550 | ||
| 551 | translate_assertion(MAcc, fact(Expr,_Pos), NewMAcc) :- | |
| 552 | translate_e_p(Expr, TExpr), | |
| 553 | asserta(assertion(Expr)), | |
| 554 | extend_machine_acc(assertions, MAcc, TExpr, NewMAcc). | |
| 555 | ||
| 556 | % Signature facts: Identifiers may refer to the signature and are joined with 'this'. | |
| 557 | % We then need a universal quantification using 'this'. | |
| 558 | translate_signature_fact(TSignatureName, MAcc, Expr, NewMAcc) :- | |
| 559 | alloy_expr_contains_join(Expr), | |
| 560 | 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 | |
| 561 | ThisID = identifier(none,'this'), | |
| 562 | TImplication = implication(none,subset(none,set_extension(none,[ThisID]),TSignatureName),TExpr), | |
| 563 | FORALL = forall(none,[ThisID],TImplication), | |
| 564 | extend_machine_acc(properties, MAcc, FORALL, NewMAcc). | |
| 565 | translate_signature_fact(_TSignatureName, MAcc, Expr, NewMAcc) :- | |
| 566 | translate_e_p(Expr, TExpr), | |
| 567 | extend_machine_acc(properties, MAcc, TExpr, NewMAcc). | |
| 568 | ||
| 569 | % TO DO: write generic AST traversal predicate | |
| 570 | alloy_expr_contains_join(AndOr) :- | |
| 571 | AndOr =.. [Functor,ListOfAsts,_Pos], | |
| 572 | !, | |
| 573 | member(Functor, [and,or]), | |
| 574 | member(Ast, ListOfAsts), | |
| 575 | alloy_expr_contains_join(Ast), | |
| 576 | !. | |
| 577 | %alloy_expr_contains_join(identifier('this',_,_)). | |
| 578 | alloy_expr_contains_join(join(_,_,_Type,_Pos)). | |
| 579 | % alloy_expr_contains_join_with_this(join(Arg1,Arg2,_Type,_Pos)) :- | |
| 580 | % Arg1 = identifier('this',_,_) ; Arg2 = identifier('this',_,_). | |
| 581 | alloy_expr_contains_join(Expr) :- | |
| 582 | Expr =.. [_Functor,Arg1,Arg2,_Type,_Pos], | |
| 583 | !, | |
| 584 | ( alloy_expr_contains_join(Arg1) -> | |
| 585 | true | |
| 586 | ; alloy_expr_contains_join(Arg2) | |
| 587 | ). | |
| 588 | alloy_expr_contains_join(Expr) :- | |
| 589 | Expr =.. [_Functor,Arg,_Type,_Pos], | |
| 590 | alloy_expr_contains_join(Arg). | |
| 591 | alloy_expr_contains_join(Expr) :- | |
| 592 | Expr =.. [Functor,_Params,Fields,Body,_Type,_POS], | |
| 593 | member(Functor, [all,no,some,one,lone,comprehension]), | |
| 594 | ( alloy_expr_contains_join(Body) -> | |
| 595 | true | |
| 596 | ; member(F, Fields), | |
| 597 | alloy_expr_contains_join(F) -> | |
| 598 | true | |
| 599 | ). | |
| 600 | ||
| 601 | % translate fun NAME Decls { Body } or pred Name Decls { Body } | |
| 602 | translate_function(MAcc, FunctionOrPredicate, NewMAcc) :- | |
| 603 | FunctionOrPredicate =.. [Functor,Name,Params,Decls,Body,POS], | |
| 604 | alloy_to_b_operator(Functor, BFunctor), | |
| 605 | maplist(translate_e_p, Params, TParams), | |
| 606 | % identifier like 'this' are singleton sets, parameters have to be identifiers | |
| 607 | maplist(strip_singleton_set, TParams, TTParams), | |
| 608 | maplist(translate_function_field, Decls, TDecls), | |
| 609 | translate_e_p(Body, TBody), | |
| 610 | translate_pos(POS, BPOS), | |
| 611 | ( Functor == function | |
| 612 | -> | |
| 613 | ( TDecls == [] | |
| 614 | -> | |
| 615 | TResult = TBody % no need to create set comprehension | |
| 616 | ; % create {temp | TDecls & temp : TBody } | |
| 617 | append(TDecls, [member(none,identifier(none,'_fun_res_'),TBody)], BehaviorList), | |
| 618 | join_untyped_ast_nodes(conjunct, BehaviorList, Behavior), | |
| 619 | TResult = comprehension_set(BPOS,[identifier(none,'_fun_res_')],Behavior) | |
| 620 | ), | |
| 621 | UAst =.. [BFunctor,BPOS,Name,TTParams,TResult] | |
| 622 | ; append(TDecls, [TBody], BehaviorList), | |
| 623 | join_untyped_ast_nodes(conjunct, BehaviorList, Behavior), | |
| 624 | UAst =.. [BFunctor,BPOS,Name,TTParams,Behavior] | |
| 625 | ), | |
| 626 | ( TTParams == [] -> asserta(definition_without_param(Name)); true), | |
| 627 | extend_machine_acc(definitions, MAcc, UAst, NewMAcc). | |
| 628 | ||
| 629 | ||
| 630 | % ------------ | |
| 631 | ||
| 632 | % command utilities | |
| 633 | get_command_pos(Command,POS) :- arg(8,Command,POS). | |
| 634 | is_command_id(ID,Command) :- arg(7,Command,Idx), | |
| 635 | (Idx = index(I) -> ID=I | |
| 636 | ; functor(Command,F,Arity),add_internal_error('Not a command: ',F/Arity:Idx:Command),fail). | |
| 637 | ||
| 638 | get_command_scopes(Command, GlobalScope, ExactScopes, UpBoundScopes, BitWidth, MaxSeq) :- | |
| 639 | Command =.. [_Functor,_Body,global_scope(TGlobalScope), | |
| 640 | exact_scopes(ExactScopes),upper_bound_scopes(UpBoundScopes),BitWidth,MaxSeq|_], | |
| 641 | !, | |
| 642 | ( (TGlobalScope == -1, ExactScopes == [], UpBoundScopes == []) | |
| 643 | -> default_upper_bound_scope(DefaultScope), | |
| 644 | debug_format(19, 'Applying default global scope of ~w', [DefaultScope]), | |
| 645 | GlobalScope = DefaultScope | |
| 646 | ; GlobalScope = TGlobalScope | |
| 647 | ), | |
| 648 | debug_format(19, 'Command scopes: global=~w, exact=~w, upbound=~w,bitwidth=~w~n,maxseq=~w~n', | |
| 649 | [GlobalScope,ExactScopes,UpBoundScopes,BitWidth,MaxSeq]). | |
| 650 | get_command_scopes(Command, -1, [], [], none, none) :- | |
| 651 | add_error(alloy2b, 'Cannot process Alloy Command:', Command). | |
| 652 | ||
| 653 | % ------------ | |
| 654 | ||
| 655 | get_command_names(CmdNames) :- | |
| 656 | get_skipped_command_names(Skipped), | |
| 657 | get_translated_command_names(Translated), | |
| 658 | append(Skipped, Translated, CmdNames). | |
| 659 | ||
| 660 | get_skipped_command_names(SkippedCmds) :- | |
| 661 | findall(Name, skipped_command(_,Name), SkippedCmds). | |
| 662 | ||
| 663 | get_translated_command_names(SkippedCmds) :- | |
| 664 | findall(Name, translated_command(_,Name), SkippedCmds). | |
| 665 | ||
| 666 | %% translate_command(+MainId, +MainCommand, +MAcc, +Command, -NewMAcc). | |
| 667 | % Has a counter for run and check commands to have a coherent enumeration, which is important | |
| 668 | % for reloading machines for a specific command. | |
| 669 | translate_commands(MainId, MainCommand, MAcc, Commands, NewMAcc) :- | |
| 670 | translate_commands(MainId, MainCommand, MAcc, Commands, 0, 0, NewMAcc). | |
| 671 | ||
| 672 | %% translate_commands(+MainId, +MainCommand, +MAcc, +Commands, +AmountOfRun, +AmounfOfCheck, -NewMAcc). | |
| 673 | translate_commands(_, _, MAcc, [], _, _, MAcc). | |
| 674 | translate_commands(MainId, MainCommand, MAcc, [Command|T], Run, Check, NewMAcc) :- | |
| 675 | translate_command(MainId, MainCommand, MAcc, Command, Run, Check, NewRun, NewCheck, NewMAcc1), | |
| 676 | translate_commands(MainId, MainCommand, NewMAcc1, T, NewRun, NewCheck, NewMAcc). | |
| 677 | ||
| 678 | ||
| 679 | ||
| 680 | %% translate_command(+MainId, +MainCommand, +MAcc, +Command, +Run, +Check, -NewRun, -NewCheck, -NewMAcc). | |
| 681 | % Translates a command if it has the same scope as the main command. | |
| 682 | % Otherwise, a command is skipped for translation and not part of the resulting B machine. | |
| 683 | % Uses global states translated_command/2 and skipped_command/2. In both terms, the first argument is the overall command index. | |
| 684 | % Here, we count indices for run and check independently in order to have a naming that is useful for the user. | |
| 685 | translate_command(MainId, MainCommand, MAcc, Command, Run, Check, NewRun, NewCheck, NewMAcc) :- | |
| 686 | Command =.. [Functor,_,GlobalScope,ExactScopes,UpBoundScopes,BitWidth,MaxSeq,_,Pos], | |
| 687 | ( atom_concat(check, _, Functor) | |
| 688 | -> NewRun = Run, | |
| 689 | NewCheck is Check + 1, | |
| 690 | CommandId = Check | |
| 691 | ; NewCheck = Check, | |
| 692 | NewRun is Run + 1, | |
| 693 | CommandId = Run | |
| 694 | ), | |
| 695 | functor(MainCommand, MainFunctor, _), | |
| 696 | % skip if not main command and scopes do not match with main command scopes | |
| 697 | \+ (MainFunctor == Functor, CommandId == MainId), | |
| 698 | \+ MainCommand =.. [_,_,GlobalScope,ExactScopes,UpBoundScopes,BitWidth,MaxSeq,_,_], | |
| 699 | !, | |
| 700 | get_command_name(Functor, CommandId, CmdName), | |
| 701 | is_command_id(ID,Command), | |
| 702 | asserta(skipped_command(ID,CmdName)), | |
| 703 | ajoin(['Skipping Alloy ',Functor, ' command ',CommandId,', scopes incompatible with main command: '],Msg), | |
| 704 | translate_pos(Pos,BPos), | |
| 705 | add_message(alloy2b_command_skipped,Msg,[GlobalScope,ExactScopes,UpBoundScopes,BitWidth,MaxSeq],BPos), | |
| 706 | NewMAcc=MAcc. | |
| 707 | translate_command(_,_,MAcc, Command, Run, Check, NewRun, NewCheck, NewMAcc) :- | |
| 708 | Command =.. [Functor,Body|_], | |
| 709 | get_command_pos(Command,POS), | |
| 710 | % if a model does not use sequences or all commands have a common scope and we are not in proof mode, we translate all commands | |
| 711 | !, | |
| 712 | is_command_id(ID,Command), | |
| 713 | ( Functor = check | |
| 714 | -> NewRun = Run, | |
| 715 | NewCheck is Check + 1, | |
| 716 | CommandId = Check | |
| 717 | ; Functor = run, | |
| 718 | NewCheck = Check, | |
| 719 | NewRun is Run + 1, | |
| 720 | CommandId = Run | |
| 721 | ), | |
| 722 | get_command_name(Functor, CommandId, CmdName), | |
| 723 | asserta(translated_command(ID,CmdName)), | |
| 724 | translate_command_aux(MAcc, Functor, Body, POS, CommandId, NewMAcc). | |
| 725 | translate_command(_,_,MAcc, Command, _, _, _, _, MAcc) :- | |
| 726 | add_error(alloy2b,'Unknown Alloy command (be sure Alloy2B parser library is up-to-date):', Command). | |
| 727 | ||
| 728 | translate_command_aux(MAcc, Functor, Body, POS, CommandId, NewMAcc) :- | |
| 729 | debug_println(19, translating_command(Functor)), | |
| 730 | translate_pos(POS, BPOS), | |
| 731 | ( get_preference(alloy_translation_for_proof, true) | |
| 732 | -> remove_negations_of_check_command(POS, Functor, Body, NBody1), | |
| 733 | remove_facts_and_assertions_from_command(NBody1, NBody), | |
| 734 | translate_e_p(NBody, TBody), | |
| 735 | extend_machine_acc(assertions, MAcc, TBody, NewMAcc) | |
| 736 | ; remove_facts_and_assertions_from_command(Body, NBody), | |
| 737 | translate_e_p(NBody, TBody), | |
| 738 | number_codes(CommandId, CCommandId), | |
| 739 | atom_codes(ACommandId, CCommandId), | |
| 740 | atom_concat(Functor, ACommandId, OperationName), | |
| 741 | Operation = operation(BPOS,identifier(BPOS,OperationName),[],[],precondition(BPOS,TBody,skip(none))), | |
| 742 | extend_machine_acc(operations, MAcc, Operation, NewMAcc) | |
| 743 | ). | |
| 744 | ||
| 745 | remove_facts_and_assertions_from_list([], []). | |
| 746 | remove_facts_and_assertions_from_list([AlloyTerm|T], NT) :- | |
| 747 | (fact(AlloyTerm); assertion(AlloyTerm)), | |
| 748 | !, | |
| 749 | debug_println(19, remove_facts_and_assertions_from_command), | |
| 750 | remove_facts_and_assertions_from_list(T, NT). | |
| 751 | remove_facts_and_assertions_from_list([AlloyTerm|T], [AlloyTerm|NT]) :- | |
| 752 | remove_facts_and_assertions_from_list(T, NT). | |
| 753 | ||
| 754 | %% remove_facts_and_assertions_from_command(AlloyTerm, NAlloyTerm). | |
| 755 | % Facts and assertions are inlined in Alloy commands by Alloy's parser. | |
| 756 | % We here remove facts and assertions from a command's body since they are translated as machine properties. | |
| 757 | remove_facts_and_assertions_from_command(and(AlloyTerms,APOS), NAlloyConj) :- | |
| 758 | !, | |
| 759 | remove_facts_and_assertions_from_list(AlloyTerms, NAlloyTerms), | |
| 760 | ( NAlloyTerms = [SingleTerm] | |
| 761 | -> NAlloyConj = SingleTerm | |
| 762 | ; NAlloyConj = and(NAlloyTerms,APOS) | |
| 763 | ). | |
| 764 | remove_facts_and_assertions_from_command(AlloyTerm, AlloyTerm). | |
| 765 | ||
| 766 | % We need to remove the negation of assertions stated in a check command when | |
| 767 | % translating to the assertions to prove in AterlierB. | |
| 768 | remove_negations_of_check_command(POS,check, Body, NBody) :- | |
| 769 | Body= and(List,APos), | |
| 770 | remove_negations_of_check_command_list(POS, List, NList), | |
| 771 | NBody = and(NList,APos). | |
| 772 | remove_negations_of_check_command(_, run, Body, Body). | |
| 773 | ||
| 774 | remove_negations_of_check_command_list(_, [], []). | |
| 775 | remove_negations_of_check_command_list(pos(_, CommandCol), [AlloyTerm|T], NList) :- | |
| 776 | get_alloy_position(AlloyTerm, APOS), | |
| 777 | APOS = pos(_, Col), | |
| 778 | Col >= CommandCol, | |
| 779 | % filter those assertions stated in the command (do not remove negations of inlined assertions) | |
| 780 | !, | |
| 781 | remove_negation_alloy_term(AlloyTerm, NewAlloyTerm), | |
| 782 | remove_negations_of_check_command_list(pos(_, CommandCol), T, NT), | |
| 783 | NList = [NewAlloyTerm|NT]. | |
| 784 | remove_negations_of_check_command_list(POS, [AlloyTerm|T], [AlloyTerm|NT]) :- | |
| 785 | remove_negations_of_check_command_list(POS, T, NT). | |
| 786 | ||
| 787 | remove_negation_alloy_term(not(AlloyTerm,_,_), AlloyTerm) :- | |
| 788 | !. | |
| 789 | remove_negation_alloy_term(AlloyTerm, AlloyTerm). | |
| 790 | ||
| 791 | translate_scopes_for_command(Command,SignatureNames,ResPredicate) :- | |
| 792 | get_command_scopes(Command, GlobalScope, ExactScopes, UpBoundScopes, _BitWidth, _CmdMaxSeq), | |
| 793 | maxseq(MaxSeq), | |
| 794 | % global scope, exact scopes and bitwidth | |
| 795 | % We do not need to set the bitwidth since we have real integers in B. | |
| 796 | ResPredicate = conjunct(none,SeqScopePred,conjunct(none,TScopes,TGlobalScopes)), | |
| 797 | % translate exact and upper bound scopes first | |
| 798 | translate_exact_and_upper_bound_scopes(0, ExactScopes, UpBoundScopes, EUSignatureNames, TScopes, OrdSigCounter1), | |
| 799 | % if present, define the global scope for the remaining signatures | |
| 800 | translate_global_scope(OrdSigCounter1, GlobalScope, SignatureNames, EUSignatureNames, TGlobalScopes, _), | |
| 801 | translate_seq_scopes(MaxSeq, SeqScopePred). | |
| 802 | ||
| 803 | translate_seq_scopes(MaxSeq, ScopePred) :- | |
| 804 | findall((Seq,MaxSeq), is_seq(Seq), Seqs), | |
| 805 | maplist(generate_leq_scope_predicate, Seqs, ScopePreds), | |
| 806 | join_predicates(conjunct, ScopePreds, ScopePred). | |
| 807 | ||
| 808 | % no exact scopes defined | |
| 809 | translate_exact_and_upper_bound_scopes(OrdSigCounter, [], [], ExactSigNames, TGlobalScopes, OrdSigCounter) :- | |
| 810 | !, | |
| 811 | ExactSigNames = [], | |
| 812 | TGlobalScopes = truth(none). | |
| 813 | translate_exact_and_upper_bound_scopes(OrdSigCounter, ExactScopes, UpBoundScopes, SignatureNames, TScopes, NewOrdSigCounter) :- | |
| 814 | trans_exact_or_upbnd_scopes(upper, OrdSigCounter, UpBoundScopes, [], UpBoundSigNames, [], TempTUpScopes, OrdSigCnt1), | |
| 815 | trans_exact_or_upbnd_scopes(exact, OrdSigCnt1, ExactScopes, [], ExactSigNames, [], TempTExactScopes, NewOrdSigCounter), | |
| 816 | append(TempTUpScopes, TempTExactScopes, TempTScopes), | |
| 817 | append(ExactSigNames, UpBoundSigNames, SignatureNames), | |
| 818 | join_predicates(conjunct, TempTScopes, TScopes). | |
| 819 | ||
| 820 | trans_exact_or_upbnd_scopes(_, OrdSigCounter, [], NamesAcc, NamesAcc, TScopeAcc, TScopeAcc, OrdSigCounter). | |
| 821 | trans_exact_or_upbnd_scopes(ScopeType, OrdSigCounter, [(SigName,Scope)|T], NameAcc, ExactSigNames, TScopeAcc, TempTExactScopes, NewOrdSigCnt) :- | |
| 822 | is_ordered_signature(SigName), | |
| 823 | !, | |
| 824 | define_ordered_signature_as_integer_set(OrdSigCounter, SigName, Scope, TScope, Cnt1), | |
| 825 | trans_exact_or_upbnd_scopes(ScopeType, Cnt1, T, [SigName|NameAcc], ExactSigNames, [TScope|TScopeAcc], TempTExactScopes, NewOrdSigCnt). | |
| 826 | trans_exact_or_upbnd_scopes(exact, OrdSigCounter, [(SigName,Scope)|T], NameAcc, ExactSigNames, TScopeAcc, TempTExactScopes, NewOrdSigCnt) :- | |
| 827 | generate_exact_scope_predicate((SigName,Scope), TScope), | |
| 828 | trans_exact_or_upbnd_scopes(exact, OrdSigCounter, T, [SigName|NameAcc], ExactSigNames, [TScope|TScopeAcc], TempTExactScopes, NewOrdSigCnt). | |
| 829 | trans_exact_or_upbnd_scopes(upper, OrdSigCounter, [(SigName,Scope)|T], NameAcc, ExactSigNames, TScopeAcc, TempTExactScopes, NewOrdSigCnt) :- | |
| 830 | generate_leq_scope_predicate((SigName,Scope), TScope), | |
| 831 | trans_exact_or_upbnd_scopes(upper, OrdSigCounter, T, [SigName|NameAcc], ExactSigNames, [TScope|TScopeAcc], TempTExactScopes, NewOrdSigCnt). | |
| 832 | ||
| 833 | generate_exact_scope_predicate((SigName,Scope), TScopePred) :- | |
| 834 | translate_e_p(SigName, TSignatureName), | |
| 835 | % debug_format(19,'Exact scope for SignatureName=~w with scope ~w~n',[SigName,Scope]), | |
| 836 | TScopePred = equal(none,card(none,TSignatureName),integer(none,Scope)). | |
| 837 | generate_leq_scope_predicate((SigName,Scope), TScopePred) :- | |
| 838 | translate_e_p(SigName, TSignatureName), | |
| 839 | TScopePred = less_equal(none,card(none,TSignatureName),integer(none,Scope)). | |
| 840 | ||
| 841 | define_ordered_signatures_as_integer_set([], OrdSigCounter, _, [], OrdSigCounter). | |
| 842 | define_ordered_signatures_as_integer_set([TSignatureName|T], OrdSigCounter, Scope, [TScope|TScopes], NewOrdSigCounter) :- | |
| 843 | define_ordered_signature_as_integer_set(OrdSigCounter, TSignatureName, Scope, TScope, OrdSigCounter1), | |
| 844 | define_ordered_signatures_as_integer_set(T, OrdSigCounter1, Scope, TScopes, NewOrdSigCounter). | |
| 845 | ||
| 846 | define_ordered_signature_as_integer_set(OrdSigCounter, TSignatureName, Scope, TScope, NewOrdSigCounter) :- | |
| 847 | NewOrdSigCounter is OrdSigCounter+Scope, | |
| 848 | UpBound is NewOrdSigCounter-1, | |
| 849 | % TSignatureName = OrdSigCounter...UpBound | |
| 850 | TScope = equal(none,identifier(none,TSignatureName), | |
| 851 | interval(none,integer(none,OrdSigCounter),integer(none,UpBound))). | |
| 852 | ||
| 853 | % translate_global_scope(inputCounter,inputGlobalScope,inputSigNames,inputExactSigNames, OutPredicate,OutNewCounter) | |
| 854 | translate_global_scope(OrdSigCounter, -1, _, _, TGlobalScopes, OrdSigCounter) :- | |
| 855 | !, | |
| 856 | TGlobalScopes = truth(none). % no global scope defined | |
| 857 | translate_global_scope(OrdSigCounter, GlobalScope, SignatureNames, ExactSigNames, | |
| 858 | TGlobalScopes, NewOrdSigCounter) :- | |
| 859 | split_ordered_unordered_signatures(SignatureNames, ExactSigNames, OrderedSigNames, RestSignatureNames), | |
| 860 | translate_global_scope_aux(RestSignatureNames, GlobalScope, [], TempTGlobalScopes), | |
| 861 | join_predicates(conjunct, TempTGlobalScopes, TTGlobalScopes), | |
| 862 | % ordered signatures are a subset of integers, OrdSigCounter: from which number on can we assign objects | |
| 863 | define_ordered_signatures_as_integer_set(OrderedSigNames, OrdSigCounter, GlobalScope, TOrderedScopes, NewOrdSigCounter), | |
| 864 | join_predicates(conjunct, [TTGlobalScopes|TOrderedScopes], TGlobalScopes). | |
| 865 | ||
| 866 | translate_global_scope_aux([], _, Acc, Acc). | |
| 867 | translate_global_scope_aux([SignatureName|T], GlobalScope, Acc, TGlobalScopes) :- | |
| 868 | \+ abstract_sig(SignatureName), | |
| 869 | translate_e_p(SignatureName, TSignatureName), | |
| 870 | TScope = less_equal(none,card(none,TSignatureName),integer(none,GlobalScope)), | |
| 871 | translate_global_scope_aux(T, GlobalScope, [TScope|Acc], TGlobalScopes). | |
| 872 | translate_global_scope_aux([_|T], GlobalScope, Acc, TGlobalScopes) :- | |
| 873 | translate_global_scope_aux(T, GlobalScope, Acc, TGlobalScopes). | |
| 874 | ||
| 875 | split_ordered_unordered_signatures(SNames, ExactSNames, OSNames, Rest) :- | |
| 876 | split_ordered_unordered_signatures(SNames, [], [], TOSNames, TRest), | |
| 877 | % remove exact signatures which are defined separately | |
| 878 | subtract(TOSNames, ExactSNames, OSNames), | |
| 879 | subtract(TRest, ExactSNames, Rest). | |
| 880 | ||
| 881 | split_ordered_unordered_signatures([], OAcc, RAcc, OAcc, RAcc). | |
| 882 | split_ordered_unordered_signatures([SName|T], OAcc, RAcc, OSNames, Rest) :- | |
| 883 | is_ordered_signature(SName), | |
| 884 | \+ member(SName, OAcc), | |
| 885 | !, | |
| 886 | split_ordered_unordered_signatures(T, [SName|OAcc], RAcc, OSNames, Rest). | |
| 887 | split_ordered_unordered_signatures([SName|T], OAcc, RAcc, OSNames, Rest) :- | |
| 888 | \+ is_ordered_signature(SName), | |
| 889 | \+ member(SName, RAcc), | |
| 890 | !, | |
| 891 | split_ordered_unordered_signatures(T, OAcc, [SName|RAcc], OSNames, Rest). | |
| 892 | split_ordered_unordered_signatures([_|T], OAcc, RAcc, OSNames, Rest) :- | |
| 893 | split_ordered_unordered_signatures(T, OAcc, RAcc, OSNames, Rest). | |
| 894 | ||
| 895 | % signature in (subset) | |
| 896 | define_sig_as_set_or_constant(MAcc, Name, Options, POS, NewMAcc) :- | |
| 897 | memberchk(subset(Parents), Options), | |
| 898 | !, | |
| 899 | % maplist(assert_extending_signature(Name),Parents) , % subset signatures do not need to be distinct | |
| 900 | translate_pos(POS, BPOS), | |
| 901 | define_sig_as_set_or_constant_aux(constants, MAcc, Name, Options, BPOS, MAcc1), | |
| 902 | % TO DO: consider several parents -> we need the universe type | |
| 903 | Parents = [Parent|_], | |
| 904 | translate_e_p(Name, TName), | |
| 905 | translate_e_p(Parent, TParent), | |
| 906 | TNode = subset(BPOS,TName,TParent), | |
| 907 | extend_machine_acc(properties, MAcc1, TNode, NewMAcc). | |
| 908 | % signature extends | |
| 909 | define_sig_as_set_or_constant(MAcc, Name, Options, POS, NewMAcc) :- | |
| 910 | member(subsig(Parent), Options), | |
| 911 | !, | |
| 912 | ( member(one, Options) -> | |
| 913 | One = one | |
| 914 | ; One = set | |
| 915 | ), | |
| 916 | assert_extending_signature(Name, Parent, One), | |
| 917 | translate_pos(POS, BPOS), | |
| 918 | define_sig_as_set_or_constant_aux(constants, MAcc, Name, Options, BPOS, MAcc1), | |
| 919 | translate_e_p(Name, TName), | |
| 920 | translate_e_p(Parent, TParent), | |
| 921 | TNode = subset(BPOS,TName,TParent), | |
| 922 | extend_machine_acc(properties, MAcc1, TNode, NewMAcc). | |
| 923 | % default signature, but we introduced an artifical parent type, i.e., a deferred set in B | |
| 924 | define_sig_as_set_or_constant(MAcc, Name, Options, POS, NewMAcc) :- | |
| 925 | translate_pos(POS, BPOS), | |
| 926 | artificial_parent_type(Name, ParentId, _), | |
| 927 | !, | |
| 928 | translate_e_p(Name, TName), | |
| 929 | TNode = subset(BPOS,TName,ParentId), | |
| 930 | extend_machine_acc(properties, MAcc, TNode, MAcc1), | |
| 931 | define_sig_as_set_or_constant_aux(constants, MAcc1, Name, Options, BPOS, NewMAcc). | |
| 932 | % default signature | |
| 933 | define_sig_as_set_or_constant(MAcc, Name, Options, POS, NewMAcc) :- | |
| 934 | translate_pos(POS, BPOS), | |
| 935 | define_sig_as_set_or_constant_aux(sets, MAcc, Name, Options, BPOS, NewMAcc). | |
| 936 | ||
| 937 | define_sig_as_set_or_constant_aux(sets, MAcc, Name, Options, BPOS, NewMAcc) :- | |
| 938 | member(one, Options), | |
| 939 | !, | |
| 940 | atom_concat('_', Name, EnumElement), | |
| 941 | % TO DO: couldn't figure out untyped ast of enumerated set, define enumerated set S = {_S} instead of constant etc. | |
| 942 | extend_machine_acc(sets, MAcc, deferred_set(BPOS,Name), MAcc1), | |
| 943 | extend_machine_acc(constants, MAcc1, identifier(BPOS,EnumElement), MAcc2), | |
| 944 | extend_machine_acc(properties, MAcc2, equal(BPOS,identifier(BPOS,Name),set_extension(BPOS,[identifier(BPOS,EnumElement)])), NewMAcc). | |
| 945 | define_sig_as_set_or_constant_aux(sets, MAcc, Name, Options, BPOS, NewMAcc) :- | |
| 946 | member(some, Options), | |
| 947 | !, | |
| 948 | extend_machine_acc(sets, MAcc, deferred_set(BPOS,Name), MAcc1), | |
| 949 | extend_machine_acc(properties, MAcc1, greater_equal(BPOS,card(BPOS,identifier(BPOS,Name)),integer(BPOS,1)), NewMAcc). | |
| 950 | define_sig_as_set_or_constant_aux(sets, MAcc, Name, Options, BPOS, NewMAcc) :- | |
| 951 | member(lone, Options), | |
| 952 | !, | |
| 953 | extend_machine_acc(sets, MAcc, deferred_set(BPOS,Name), MAcc1), | |
| 954 | extend_machine_acc(properties, MAcc1, less_equal(BPOS,card(BPOS,identifier(BPOS,Name)),integer(BPOS,1)), NewMAcc). | |
| 955 | define_sig_as_set_or_constant_aux(sets, MAcc, Name, _Options, BPOS, NewMAcc) :- | |
| 956 | extend_machine_acc(sets, MAcc, deferred_set(BPOS,Name), NewMAcc). | |
| 957 | define_sig_as_set_or_constant_aux(constants, MAcc, Name, _Options, BPOS, NewMAcc) :- | |
| 958 | extend_machine_acc(constants, MAcc, identifier(BPOS,Name), NewMAcc). | |
| 959 | ||
| 960 | % -------- | |
| 961 | % Semantic translation rules: translate expression or predicate | |
| 962 | % -------- | |
| 963 | translate_e_p2(A, TA) :- %% functor(A,F,N),format('~n TRANSLATE: ~w/~w : ~w ~n',[F,N,A]), | |
| 964 | translate_quantifier_e(A, TA), | |
| 965 | !. | |
| 966 | translate_e_p2(A, TA) :- | |
| 967 | translate_cst_e_p(A, TA), | |
| 968 | !. | |
| 969 | translate_e_p2(A, TA) :- | |
| 970 | translate_unary_e_p(A, TA), | |
| 971 | !. | |
| 972 | translate_e_p2(A, TA) :- | |
| 973 | translate_binary_e_p(A, TA), | |
| 974 | !. | |
| 975 | translate_e_p2(A, TA) :- | |
| 976 | translate_if_then_else(A, TA), | |
| 977 | !. | |
| 978 | translate_e_p2(A, _) :- | |
| 979 | add_error(load_alloy_model, 'Translation failed for:', A), | |
| 980 | fail. | |
| 981 | ||
| 982 | translate_e_p(A, TA) :- | |
| 983 | translate_e_p2(A, TA), | |
| 984 | check_valid_raw_translation(A,TA). | |
| 985 | ||
| 986 | :- load_files(library(system), [when(compile_time), imports([environ/2])]). | |
| 987 | :- if(environ(prob_safe_mode,true)). | |
| 988 | check_valid_raw_translation(A,Raw) :- \+ ground(Raw), | |
| 989 | add_error(alloy2b,'Non-ground raw AST:',Raw,Raw), | |
| 990 | write(A),nl, trace, translate_e_p2(A,_), | |
| 991 | fail. | |
| 992 | :- endif. | |
| 993 | check_valid_raw_translation(_,_). | |
| 994 | % Translation in the context where we expect an integer | |
| 995 | % This is the E_{int} translation function in the article | |
| 996 | % The following rule is not necessary: untyped_b_ast_to_integer will peel off set extensions | |
| 997 | %translate_e_p_integer(identifier(ID,_Type,POS), identifier(BPOS,ID)) :- %Type=integer, ? | |
| 998 | % is_singleton_set(ID),!, | |
| 999 | % translate_pos(POS, BPOS). | |
| 1000 | translate_e_p_integer(integer(A,POS), integer(BPOS,A)) :- | |
| 1001 | !, | |
| 1002 | translate_pos(POS, BPOS). | |
| 1003 | translate_e_p_integer(A, BAstInt) :- | |
| 1004 | translate_e_p(A, BAst), | |
| 1005 | untyped_b_ast_to_integer(BAst, BAstInt). | |
| 1006 | ||
| 1007 | untyped_b_ast_to_integer(integer(BPOS,A), integer(BPOS,A)) :- | |
| 1008 | !. | |
| 1009 | untyped_b_ast_to_integer(set_extension(_,[Single]), Single) :- | |
| 1010 | !. | |
| 1011 | % Alloy sums the elements of sets of integers so we can use SIGMA which also strips singleton sets like the MU operator. | |
| 1012 | % If preference alloy_strict_integers is set, we only accept singleton sets as integers and throw a WD error otherwise. | |
| 1013 | untyped_b_ast_to_integer(BAst, BAstInt) :- | |
| 1014 | get_preference(alloy_strict_integers, Strict), | |
| 1015 | Strict == false, | |
| 1016 | !, | |
| 1017 | get_b_position(BAst, BPOS), | |
| 1018 | check_position(BPOS,untyped_b_ast_to_integer), | |
| 1019 | BAstInt = general_sum(BPOS,[identifier(BPOS,z)],member(BPOS,identifier(BPOS,z),BAst),identifier(BPOS,z)). | |
| 1020 | untyped_b_ast_to_integer(BAst, BAstInt) :- | |
| 1021 | get_b_position(BAst, BPOS), | |
| 1022 | check_position(BPOS,untyped_b_ast_to_integer), | |
| 1023 | BAstInt = mu(BPOS,BAst). | |
| 1024 | ||
| 1025 | ||
| 1026 | ||
| 1027 | % Translation in the context where we expect a singleton set. | |
| 1028 | % Otherwise, a well-definedness error is thrown. | |
| 1029 | % This is the E_{one} translation function in the article. | |
| 1030 | % Note that the arguments are already translated (using \semE{.} in the article). | |
| 1031 | translate_e_p_one(set_extension(_,[One]), Res) :- | |
| 1032 | !, | |
| 1033 | Res = One. | |
| 1034 | translate_e_p_one(BAst, mu(none,BAst)). | |
| 1035 | ||
| 1036 | % construct_choose(TSetA,external_function_call(none,'CHOOSE',[TSetA],string(none,'a member of X'),TypeParams,Decl)) :- | |
| 1037 | % % format of raw AST of CHOOSE copied from btype2 | |
| 1038 | % TypeParams = rewrite_protected([identifier(none,T)]), | |
| 1039 | % Decl = rewrite_protected(total_function(none,pow_subset(none,identifier(none,T)),identifier(none,T))). | |
| 1040 | translate_if_then_else(if_then_else(ConditionPred,TruthExpr,FalsityExpr,_Type,POS), TIfThenElse) :- | |
| 1041 | translate_e_p(ConditionPred, TConditionPred), | |
| 1042 | translate_e_p(TruthExpr, TTruthExpr), | |
| 1043 | translate_e_p(FalsityExpr, TFalsityExpr), | |
| 1044 | translate_pos(POS, BPOS), | |
| 1045 | get_type_and_arity_from_alloy_term(TruthExpr, Type, _), | |
| 1046 | ( ( Type = [untyped] | |
| 1047 | ; is_primitive_type(Type, _) | |
| 1048 | ) | |
| 1049 | -> | |
| 1050 | TIfThenElse = conjunct(BPOS, | |
| 1051 | implication(BPOS,TConditionPred,TTruthExpr), | |
| 1052 | implication(BPOS,negation(BPOS,TConditionPred),TFalsityExpr)) | |
| 1053 | ; TIfThenElse = if_then_else(BPOS,TConditionPred,TTruthExpr,TFalsityExpr) | |
| 1054 | ). | |
| 1055 | ||
| 1056 | translate_quantifier_e(Quantifier, TQuantifier) :- | |
| 1057 | Quantifier =.. [Functor,Params,Fields,Body,_Type,POS], | |
| 1058 | member(Functor, [all,no,some,one,lone,comprehension]), | |
| 1059 | maplist(translate_e_p, Params, TParams), | |
| 1060 | maplist(strip_singleton_set, TParams, TTParams), % strip singleton sets for parameter definition in the untyped B ast (only identifier/2 nodes allowed in there) | |
| 1061 | translate_pos(POS, BPOS), | |
| 1062 | maplist(translate_quantifier_field, Fields, TFieldsList, SingletonSetNames), | |
| 1063 | ( is_disjoint_quantifier(Fields) | |
| 1064 | -> | |
| 1065 | maplist(translate_e_p, SingletonSetNames, TSets), % TSets are the translated Fields | |
| 1066 | % encoding all_different by union(Set1,Set2,) | |
| 1067 | length(Fields, Len), | |
| 1068 | construct_all_diff(BPOS,Len,TSets, AllDiff), | |
| 1069 | join_untyped_ast_nodes(conjunct, [AllDiff|TFieldsList], TFields) | |
| 1070 | ; join_untyped_ast_nodes(conjunct, TFieldsList, TFields) | |
| 1071 | ), | |
| 1072 | translate_e_p(Body, TBody), | |
| 1073 | translate_quantifier_e_aux(BPOS, Functor, TTParams, TFields, TBody, TQuantifier), | |
| 1074 | % TO DO: retract singleton sets introduced in quantifiers on exit | |
| 1075 | maplist(retract_singleton_set(BPOS), SingletonSetNames). | |
| 1076 | ||
| 1077 | construct_all_diff(BPOS,2,[S1,S2],AllDiff) :- !, AllDiff = not_equal(BPOS,S1,S2). | |
| 1078 | construct_all_diff(BPOS,Len,TSets, AllDiff) :- | |
| 1079 | AllDiff = equal(BPOS,card(BPOS,general_union(BPOS,set_extension(BPOS,TSets))),integer(BPOS,Len)). | |
| 1080 | % encoding all_different by card(union({O1,O2,...,Ok}) = k | |
| 1081 | ||
| 1082 | ||
| 1083 | translate_quantifier_e_aux(Pos, all, TParams, TFields, TBody, forall(Pos,TParams,implication(Pos,TFields,TBody))). | |
| 1084 | translate_quantifier_e_aux(Pos, no, TParams, TFields, TBody, negation(Pos,exists(Pos,TParams,conjunct(Pos,TFields,TBody)))). | |
| 1085 | translate_quantifier_e_aux(Pos, some, TParams, TFields, TBody, exists(Pos,TParams,conjunct(Pos,TFields,TBody))). | |
| 1086 | translate_quantifier_e_aux(Pos, one, TParams, TFields, TBody, equal(Pos,card(Pos,comprehension_set(Pos,TParams,conjunct(Pos,TFields,TBody))),integer(Pos,1))). | |
| 1087 | translate_quantifier_e_aux(Pos, lone, TParams, TFields, TBody, less_equal(Pos,card(Pos,comprehension_set(Pos,TParams,conjunct(Pos,TFields,TBody))),integer(Pos,1))). | |
| 1088 | translate_quantifier_e_aux(Pos, comprehension, TParams, TFields, TBody, comprehension_set(Pos,TParams,conjunct(Pos,TFields,TBody))). | |
| 1089 | ||
| 1090 | % Translate Constants | |
| 1091 | translate_cst_e_p(iden(POS), event_b_identity(BPOS)) :- % has no Span Info ! | |
| 1092 | translate_pos(POS, BPOS). | |
| 1093 | translate_cst_e_p(identifier(Cst,_,POS), BConstruct) :- | |
| 1094 | alloy_constant_to_b(Cst, BPOS, BConstruct), | |
| 1095 | !, | |
| 1096 | translate_pos(POS, BPOS). | |
| 1097 | translate_cst_e_p(none(POS), TNone) :- | |
| 1098 | !, | |
| 1099 | translate_pos(POS, BPOS), | |
| 1100 | TNone = empty_set(BPOS). | |
| 1101 | translate_cst_e_p(this, _) :- | |
| 1102 | print('this not yet translated'), | |
| 1103 | nl, | |
| 1104 | fail. | |
| 1105 | ||
| 1106 | ||
| 1107 | alloy_constant_to_b(none, BPOS, empty_set(BPOS)). | |
| 1108 | alloy_constant_to_b('boolean''False', BPOS, boolean_false(BPOS)). | |
| 1109 | alloy_constant_to_b('boolean''True', BPOS, boolean_true(BPOS)). | |
| 1110 | alloy_constant_to_b('boolean''Bool', BPOS, bool_set(BPOS)). | |
| 1111 | ||
| 1112 | translate_unary_e_p(cast2int(Expr,_Type,POS), Result) :- | |
| 1113 | !, | |
| 1114 | translate_pos(POS, BPOS), | |
| 1115 | translate_e_p_integer(Expr, TExpr), | |
| 1116 | Result = set_extension(BPOS, [TExpr]). | |
| 1117 | translate_unary_e_p(cast2sigint(Expr,_Type,_Pos), Result) :- | |
| 1118 | % TO DO: do we need this? how is this written in Alloy? | |
| 1119 | !, | |
| 1120 | translate_e_p(Expr, TExpr), | |
| 1121 | Result = TExpr. | |
| 1122 | translate_unary_e_p(string(StringCodes,POS), Result) :- | |
| 1123 | atom_codes(String, StringCodes), | |
| 1124 | !, | |
| 1125 | translate_pos(POS, BPOS), | |
| 1126 | Result = set_extension(BPOS,[string(BPOS,String)]). | |
| 1127 | translate_unary_e_p(seq(ID), Result) :- | |
| 1128 | translate_unary_e_p(ID, TID), | |
| 1129 | !, | |
| 1130 | Result = sequence_extension(none,TID). | |
| 1131 | translate_unary_e_p(Int, Result) :- | |
| 1132 | integer(Int), % Note: this is not really a unary operator but a constant | |
| 1133 | !, | |
| 1134 | Result = integer(none,Int). | |
| 1135 | translate_unary_e_p(Term, Result) :- | |
| 1136 | ( Term = identifier(ID,type(TypeList,_),POS), | |
| 1137 | TypeList = [SigName|_] | |
| 1138 | ; Term = ID, | |
| 1139 | POS = none | |
| 1140 | ), | |
| 1141 | atom(ID), | |
| 1142 | sig_field_id(ID, SigName), | |
| 1143 | !, | |
| 1144 | atom_concat(ID, '_', NID), | |
| 1145 | atom_concat(NID, SigName, NNID), | |
| 1146 | translate_pos(POS, BPOS), | |
| 1147 | (is_singleton_set_id(NNID) | |
| 1148 | -> Result = set_extension(BPOS,[identifier(BPOS,NNID)]) | |
| 1149 | ; Result = identifier(BPOS,NNID)). | |
| 1150 | translate_unary_e_p(identifier(ID,Type,POS), Result) :- | |
| 1151 | prepend_identifier_of_module_import(ID, Type, NID), | |
| 1152 | % singleton enumerated set like S = {_S} | |
| 1153 | enumerated_set(NID), | |
| 1154 | is_singleton_set_id(NID), | |
| 1155 | !, | |
| 1156 | translate_pos(POS, BPOS), | |
| 1157 | Result = set_extension(BPOS,[identifier(BPOS,NID)]). | |
| 1158 | translate_unary_e_p(identifier(ID,Type,POS), Result) :- | |
| 1159 | prepend_identifier_of_module_import(ID, Type, NID), | |
| 1160 | is_singleton_set_id(NID), | |
| 1161 | !, | |
| 1162 | translate_pos(POS, BPOS), | |
| 1163 | Result = set_extension(BPOS,[identifier(BPOS,NID)]). | |
| 1164 | translate_unary_e_p(ID, Result) :- | |
| 1165 | atom(ID), | |
| 1166 | prepend_module_name(ID,NID), | |
| 1167 | enumerated_set(NID), | |
| 1168 | is_singleton_set_id(NID), | |
| 1169 | !, | |
| 1170 | Result = set_extension(none,[identifier(none,NID)]). | |
| 1171 | translate_unary_e_p(ID, Result) :- | |
| 1172 | atom(ID), | |
| 1173 | prepend_module_name(ID,NID), | |
| 1174 | is_singleton_set_id(NID), | |
| 1175 | !, | |
| 1176 | Result = set_extension(none,[identifier(none,NID)]). | |
| 1177 | translate_unary_e_p(integer(A,POS), Result) :- | |
| 1178 | !, | |
| 1179 | translate_pos(POS, BPOS), | |
| 1180 | Result = set_extension(BPOS,[integer(BPOS,A)]). | |
| 1181 | translate_unary_e_p(identifier('Int',_Type,POS), Result) :- | |
| 1182 | !, | |
| 1183 | translate_pos(POS, BPOS), | |
| 1184 | integer_type(IntOrInteger), | |
| 1185 | Result = integer_set(BPOS,IntOrInteger). | |
| 1186 | translate_unary_e_p(identifier(Id,_Type,POS), Result) :- | |
| 1187 | alloy_natural_id(Id, 'Natural'), | |
| 1188 | !, | |
| 1189 | translate_pos(POS, BPOS), | |
| 1190 | natural_type(NatOrNatural), | |
| 1191 | Result = integer_set(BPOS,NatOrNatural). | |
| 1192 | translate_unary_e_p(identifier(Id,_Type,POS), Result) :- | |
| 1193 | alloy_natural_id(Id, 'One'), | |
| 1194 | !, | |
| 1195 | translate_pos(POS, BPOS), | |
| 1196 | Result = set_extension(BPOS,[integer(BPOS,1)]). | |
| 1197 | translate_unary_e_p(identifier(Id,_Type,POS), Result) :- | |
| 1198 | alloy_natural_id(Id, 'Zero'), | |
| 1199 | !, | |
| 1200 | translate_pos(POS, BPOS), | |
| 1201 | Result = set_extension(BPOS,[integer(BPOS,0)]). | |
| 1202 | translate_unary_e_p(identifier('String',_,_), Result) :- | |
| 1203 | !, | |
| 1204 | Result = string_set(none). | |
| 1205 | translate_unary_e_p(identifier(ID,Type,POS), Result) :- | |
| 1206 | !, | |
| 1207 | prepend_identifier_of_module_import(ID, Type, NID), | |
| 1208 | translate_pos(POS, BPOS), | |
| 1209 | Result = identifier(BPOS,NID). | |
| 1210 | translate_unary_e_p('Int', Result) :- | |
| 1211 | !, | |
| 1212 | integer_type(IntOrInteger), | |
| 1213 | Result = integer_set(none,IntOrInteger). | |
| 1214 | translate_unary_e_p(Id, Result) :- | |
| 1215 | alloy_natural_id(Id, 'Natural'), | |
| 1216 | !, | |
| 1217 | natural_type(NatOrNatural), | |
| 1218 | Result = integer_set(none,NatOrNatural). | |
| 1219 | translate_unary_e_p(Id, Result) :- | |
| 1220 | alloy_natural_id(Id, 'One'), | |
| 1221 | !, | |
| 1222 | Result = set_extension(none,[integer(none,1)]). | |
| 1223 | translate_unary_e_p(Id, Result) :- | |
| 1224 | alloy_natural_id(Id, 'Zero'), | |
| 1225 | !, | |
| 1226 | Result = set_extension(none,[integer(none,0)]). | |
| 1227 | translate_unary_e_p(boolean(true,POS), Result) :- | |
| 1228 | !, % was boolean_true, but Alloy has no booleans | |
| 1229 | translate_pos(POS, BPOS), | |
| 1230 | Result = truth(BPOS). | |
| 1231 | translate_unary_e_p(boolean(false,POS), Result) :- | |
| 1232 | !, % was boolean_false | |
| 1233 | translate_pos(POS, BPOS), | |
| 1234 | Result = falsity(BPOS). | |
| 1235 | translate_unary_e_p(Type, Result) :- | |
| 1236 | % lhs of sequence is integer, Alloy Types are like [seqInt,A] for set(couple(INTEGER,A)) | |
| 1237 | atom(Type), | |
| 1238 | atom_prefix(seq, Type), | |
| 1239 | !, | |
| 1240 | integer_type(IntOrInteger), | |
| 1241 | Result = integer_set(none,IntOrInteger). | |
| 1242 | translate_unary_e_p(ID, Result) :- | |
| 1243 | atom(ID), | |
| 1244 | prepend_module_name(ID,NID), | |
| 1245 | !, | |
| 1246 | Result = identifier(none,NID). | |
| 1247 | translate_unary_e_p(UnaryP, TUnaryP) :- | |
| 1248 | % and/or defines a list of ast nodes | |
| 1249 | UnaryP =.. [Op,ArgList|_], | |
| 1250 | memberchk(Op, [and,or]), % translated to conjunct/disjunct | |
| 1251 | is_list(ArgList), | |
| 1252 | !, | |
| 1253 | maplist(translate_e_p, ArgList, TArgList), | |
| 1254 | join_predicates(Op, TArgList, TUnaryP). | |
| 1255 | translate_unary_e_p(UnaryP, TUnaryP) :- | |
| 1256 | UnaryP =.. [Op,Arg,_Type,POS], | |
| 1257 | member(Op, [no,one,some,lone,exactlyof,oneof,someof,loneof]), | |
| 1258 | !, | |
| 1259 | translate_e_p(Arg, TArg), | |
| 1260 | translate_pos(POS, BPOS), | |
| 1261 | translate_quantified_e(BPOS, Op, TArg, TUnaryP). | |
| 1262 | translate_unary_e_p(card(Arg,_Type,POS), set_extension(BPOS,[card(BPOS,TArg)])) :- | |
| 1263 | !, | |
| 1264 | translate_e_p(Arg, TArg), | |
| 1265 | translate_pos(POS, BPOS). | |
| 1266 | translate_unary_e_p(UnaryP, TUnaryP) :- | |
| 1267 | UnaryP =.. [Op,Arg,_Type,POS], | |
| 1268 | translate_e_p(Arg, TArg), | |
| 1269 | alloy_to_b_unary_operator(Op, BOp), | |
| 1270 | translate_pos(POS, BPOS), | |
| 1271 | TUnaryP =.. [BOp,BPOS,TArg]. | |
| 1272 | ||
| 1273 | alloy_natural_id(Id, Suffix) :- | |
| 1274 | atom(Id), | |
| 1275 | module_in_scope_but_root('util''natural', Alias), | |
| 1276 | atom_concat(Alias, '\'', Prefix), | |
| 1277 | atom_concat(Prefix, Suffix, Id). | |
| 1278 | ||
| 1279 | % support for Alloy modules to maintain unique identifiers | |
| 1280 | prepend_module_name(ID,NID) :- | |
| 1281 | atom(ID), | |
| 1282 | \+ has_module_prefix(ID), | |
| 1283 | current_module_in_scope(ModuleName), | |
| 1284 | !, | |
| 1285 | atom_concat(ModuleName, '''', ModuleNameP), | |
| 1286 | atom_concat(ModuleNameP, ID, NID). | |
| 1287 | prepend_module_name(ID,ID). | |
| 1288 | ||
| 1289 | has_module_prefix(ID) :- | |
| 1290 | atom(ID), | |
| 1291 | module_in_scope_but_root(ModuleName, Alias), | |
| 1292 | ( atom_prefix(ModuleName , ID) | |
| 1293 | ; Alias \== 'alloy2b_none', | |
| 1294 | atom_prefix(Alias, ID) | |
| 1295 | ), | |
| 1296 | !. | |
| 1297 | ||
| 1298 | prepend_identifier_of_module_import(ID, Type, NID) :- | |
| 1299 | % field names of signatures from imported modules are not unique, | |
| 1300 | % their type (the signature name) is unique though | |
| 1301 | atom(ID), | |
| 1302 | Type = type([Inner|_],_), | |
| 1303 | module_in_scope_but_root(ModuleName, Alias), | |
| 1304 | ( Alias \== 'alloy2b_none' | |
| 1305 | -> Name = Alias | |
| 1306 | ; Name = ModuleName | |
| 1307 | ), | |
| 1308 | atom_prefix(Name, Inner), | |
| 1309 | atom_concat(Name, '''', NameP), | |
| 1310 | \+ atom_prefix(NameP, ID), | |
| 1311 | !, | |
| 1312 | atom_concat(NameP, ID, NID). | |
| 1313 | prepend_identifier_of_module_import(ID, _, ID). | |
| 1314 | ||
| 1315 | %% FUNCTIONS defined by func in util: | |
| 1316 | % alloy_to_b_natural_utility_function(Name, BPOS, Params, Result). | |
| 1317 | % Special cases with no direct counterpart in B. | |
| 1318 | alloy_to_b_natural_utility_function('''ord''first', BPOS, [], set_extension(BPOS,[integer(BPOS,0)])). | |
| 1319 | alloy_to_b_natural_utility_function('''ord''last', BPOS, [], set_extension(BPOS,[max_int(BPOS)])). | |
| 1320 | alloy_to_b_natural_utility_function('''ord''next', BPOS, [P1Int], set_extension(BPOS,[add(BPOS,P1Int,integer(BPOS,1))])). | |
| 1321 | alloy_to_b_natural_utility_function('''ord''prev', BPOS, [P1Int], set_extension(BPOS,[minus(BPOS,P1Int,integer(BPOS,1))])). | |
| 1322 | alloy_to_b_natural_utility_function('''One', BPOS, [], set_extension(BPOS,[integer(BPOS,1)])). | |
| 1323 | alloy_to_b_natural_utility_function('''Zero', BPOS, [], set_extension(BPOS,[integer(BPOS,0)])). | |
| 1324 | alloy_to_b_natural_utility_function('''min', BPOS, [], set_extension(BPOS,[max(BPOS,set_extension(BPOS,[integer(BPOS,0),min_int(BPOS)]))])). | |
| 1325 | alloy_to_b_natural_utility_function('''inc', BPOS, [P1Int], set_extension(BPOS,[add(BPOS,P1Int,integer(BPOS,1))])). | |
| 1326 | alloy_to_b_natural_utility_function('''dec', BPOS, [P1Int], set_extension(BPOS,[minus(BPOS,P1Int,integer(BPOS,1))])). | |
| 1327 | ||
| 1328 | % alloy_to_b_integer_utility_function(Name, BPOS, Params, Result). | |
| 1329 | % Special cases with no direct counterpart in B. | |
| 1330 | alloy_to_b_integer_utility_function('''signum', BPOS, [P1Int], Result) :- | |
| 1331 | !, | |
| 1332 | % IF int(p) < 0 THEN -1 ELSE IF int(p) > 0 THEN 1 ELSE 0 END END | |
| 1333 | Result = if_then_else(BPOS,less(BPOS,P1Int,integer(BPOS,0)),set_extension(BPOS,[integer(BPOS,-1)]),if_then_else(BPOS,greater(BPOS,P1Int,integer(BPOS,0)),set_extension(BPOS,[integer(BPOS,1)]),set_extension(BPOS,[integer(BPOS,0)]))). | |
| 1334 | alloy_to_b_integer_utility_function('''zero', BPOS, [P1Int], Result) :- | |
| 1335 | !, | |
| 1336 | % int(p) = 0 | |
| 1337 | Result = equal(BPOS,P1Int,integer(BPOS,0)). | |
| 1338 | alloy_to_b_integer_utility_function(Name, BPOS, [P1Int], Result) :- | |
| 1339 | ( Name == '''pos', BOp = greater | |
| 1340 | ; Name == '''neg', BOp = less), | |
| 1341 | !, | |
| 1342 | translate_e_p_integer(P1Int, P1Int), | |
| 1343 | % int(p) > 0 or int(p) < 0 | |
| 1344 | Result =.. [BOp,BPOS,P1Int,integer(BPOS,0)]. | |
| 1345 | alloy_to_b_integer_utility_function(Name, BPOS, [P1Int], Result) :- | |
| 1346 | ( Name == '''nonpos', BOp = less_equal | |
| 1347 | ; Name == '''nonneg', BOp = greater_equal), | |
| 1348 | !, | |
| 1349 | translate_e_p_integer(P1Int, P1Int), | |
| 1350 | % int(p) <= 0 or int(p) >= 0 | |
| 1351 | Result =.. [BOp,BPOS,P1Int,integer(BPOS,0)]. | |
| 1352 | alloy_to_b_integer_utility_function(Name, BPOS, [P1Int,P2Int], Result) :- | |
| 1353 | ( Name == '''smaller', BOp = min | |
| 1354 | ; Name == '''larger', BOp = max), | |
| 1355 | !, | |
| 1356 | % {min({int(p1),int(p2)})} or {max({int(p1),int(p2)})} | |
| 1357 | Inner =.. [BOp,BPOS,set_extension(BPOS,[P1Int,P2Int])], | |
| 1358 | Result = set_extension(BPOS,[Inner]). | |
| 1359 | alloy_to_b_integer_utility_function(Name, BPOS, [P1Int], Result) :- | |
| 1360 | ( Name == '''nexts', BOp = greater | |
| 1361 | ; Name == '''prevs', BOp = less), | |
| 1362 | !, | |
| 1363 | % {x | x : INTEGER & x > int(p)} or {x | x : INTEGER & x < int(p)} | |
| 1364 | Inner =.. [BOp,BPOS,identifier(BPOS,x),P1Int], | |
| 1365 | integer_type(IntOrInteger), | |
| 1366 | check_position(BPOS,alloy_to_b_integer_utility_function(Name)), | |
| 1367 | Result = comprehension_set(BPOS,[identifier(BPOS,x)], | |
| 1368 | conjunct(BPOS,member(BPOS,identifier(BPOS,x),integer_set(none,IntOrInteger)),Inner)). | |
| 1369 | ||
| 1370 | %% alloy_to_b_integer_natural_utility_func(Name,Arity,BOperator,ArgType,ReturnType). | |
| 1371 | % Special cases with direct counterparts in B. | |
| 1372 | alloy_to_b_integer_natural_utility_func(FunName, Arity, BOp, ArgType, ReturnType) :- | |
| 1373 | is_util_integer_natural_func(FunName, _, AlloyOp), | |
| 1374 | ( alloy_to_b_integer_func(AlloyOp, Arity, BOp, ArgType, ReturnType) | |
| 1375 | ; alloy_to_b_integer_operator_func(AlloyOp, Arity, BOp, ArgType, ReturnType) | |
| 1376 | ; alloy_to_b_integer_to_integer_func(AlloyOp, Arity, BOp, ArgType, ReturnType) | |
| 1377 | ; alloy_to_b_operator_func(AlloyOp, Arity, BOp, ArgType, ReturnType) | |
| 1378 | ),!. | |
| 1379 | ||
| 1380 | is_util_integer_natural_func(FunName, UtilType, AlloyOp) :- | |
| 1381 | atom(FunName), | |
| 1382 | module_in_scope_but_root(ModuleName, Alias), | |
| 1383 | atom(ModuleName), | |
| 1384 | atom(Alias), | |
| 1385 | ( atom_concat(ModuleName, AlloyOp, FunName) | |
| 1386 | ; atom_concat(Alias, AlloyOp, FunName) | |
| 1387 | ), | |
| 1388 | ( ModuleName == 'util''integer', | |
| 1389 | UtilType = integer | |
| 1390 | ; ModuleName == 'util''natural', | |
| 1391 | UtilType = natural | |
| 1392 | ). | |
| 1393 | ||
| 1394 | % functions with integer arguments and result | |
| 1395 | alloy_to_b_integer_to_integer_func('''minus', 2, minus, integer, integer). | |
| 1396 | alloy_to_b_integer_to_integer_func('''plus', 2, add, integer, integer). | |
| 1397 | alloy_to_b_integer_to_integer_func('''div', 2, div, integer, integer). | |
| 1398 | alloy_to_b_integer_to_integer_func('''mul', 2, multiplication, integer, integer). | |
| 1399 | alloy_to_b_integer_to_integer_func('''rem', 2, modulo, integer, integer). | |
| 1400 | % alloy_to_b_integer_to_integer_func('''sum',sigma, integer, integer). % TO DO: translate sum | |
| 1401 | alloy_to_b_integer_to_integer_func('''add', 2, add, integer, integer). | |
| 1402 | alloy_to_b_integer_to_integer_func('''sub', 2, minus, integer, integer). | |
| 1403 | % Unary: | |
| 1404 | alloy_to_b_integer_to_integer_func('''negate', 1, unary_minus, integer, integer). | |
| 1405 | alloy_to_b_integer_to_integer_func('''next', 1, successor, integer, integer). % not sure this is called; seems to call arity 0 and use join | |
| 1406 | alloy_to_b_integer_to_integer_func('''prev', 1, predecessor, integer, integer). | |
| 1407 | ||
| 1408 | % functions with integer result but set arguments | |
| 1409 | alloy_to_b_integer_func('''min', 1, min, set, integer). | |
| 1410 | alloy_to_b_integer_func('''max', 1, max, set, integer). | |
| 1411 | alloy_to_b_integer_func('''min', 0, min_int, set, integer). % TO DO: investigate bit-width related translation | |
| 1412 | alloy_to_b_integer_func('''max', 0, max_int, set, integer). | |
| 1413 | % Note: for run Arithmetic for 6 Int the Alloy Evaluator produces {-32} for min and {+31} for max | |
| 1414 | % predicate functions with integer arguments | |
| 1415 | alloy_to_b_operator_func('''next', 0, successor, set, set). | |
| 1416 | alloy_to_b_operator_func('''prev', 0, predecessor, set, set). | |
| 1417 | ||
| 1418 | % predicate functions with integer arguments | |
| 1419 | alloy_to_b_integer_operator_func('''gt', 2, greater, integer, set). | |
| 1420 | alloy_to_b_integer_operator_func('''lt', 2, less, integer, set). | |
| 1421 | alloy_to_b_integer_operator_func('''gte', 2, greater_equal, integer, set). | |
| 1422 | alloy_to_b_integer_operator_func('''lte', 2, less_equal, integer, set). | |
| 1423 | alloy_to_b_integer_operator_func('''eq', 2, equal, integer, set). | |
| 1424 | ||
| 1425 | % Not[b] = bool(b = FALSE) | |
| 1426 | alloy_to_b_boolean_utility_function('boolean''Not', [TP1], BPOS, Result) :- | |
| 1427 | !, | |
| 1428 | Result = convert_bool(BPOS,equal(BPOS,TP1,boolean_false(BPOS))). | |
| 1429 | alloy_to_b_boolean_utility_function('boolean''isTrue', [TP1], BPOS, Result) :- | |
| 1430 | !, | |
| 1431 | Result = equal(BPOS,TP1,boolean_true(BPOS)). | |
| 1432 | alloy_to_b_boolean_utility_function('boolean''isFalse', [TP1], BPOS, Result) :- | |
| 1433 | !, | |
| 1434 | Result = equal(BPOS,TP1,boolean_false(BPOS)). | |
| 1435 | % And[a,b] = bool(a = TRUE & b = TRUE) | |
| 1436 | alloy_to_b_boolean_utility_function('boolean''And', [TP1,TP2], BPOS, Result) :- | |
| 1437 | !, | |
| 1438 | Result = convert_bool(BPOS,conjunct(BPOS,equal(BPOS,TP1,boolean_true(BPOS)),equal(BPOS,TP2,boolean_true(BPOS)))). | |
| 1439 | % Or[a,b] = bool(a = TRUE or b = TRUE) | |
| 1440 | alloy_to_b_boolean_utility_function('boolean''Or', [TP1,TP2], BPOS, Result) :- | |
| 1441 | !, | |
| 1442 | Result = convert_bool(BPOS,disjunct(BPOS,equal(BPOS,TP1,boolean_true(BPOS)),equal(BPOS,TP2,boolean_true(BPOS)))). | |
| 1443 | % Nand[a,b] = bool(a = FALSE or b = FALSE) | |
| 1444 | alloy_to_b_boolean_utility_function('boolean''Nand', [TP1,TP2], BPOS, Result) :- | |
| 1445 | !, | |
| 1446 | Result = convert_bool(BPOS,disjunct(BPOS,equal(BPOS,TP1,boolean_false(BPOS)),equal(BPOS,TP2,boolean_false(BPOS)))). | |
| 1447 | % Nor[a,b] = bool(a = FALSE & b = FALSE) | |
| 1448 | alloy_to_b_boolean_utility_function('boolean''Nor', [TP1,TP2], BPOS, Result) :- | |
| 1449 | !, | |
| 1450 | Result = convert_bool(BPOS,conjunct(BPOS,equal(BPOS,TP1,boolean_false(BPOS)),equal(BPOS,TP2,boolean_false(BPOS)))). | |
| 1451 | % Xor[a,b] = bool((a = FALSE & b = TRUE) or (a = TRUE & b = FALSE)) | |
| 1452 | alloy_to_b_boolean_utility_function('boolean''Xor', [TP1,TP2], BPOS, Result) :- | |
| 1453 | !, | |
| 1454 | LHS = conjunct(BPOS,equal(BPOS,TP1,boolean_false(BPOS)),equal(BPOS,TP2,boolean_true(BPOS))), | |
| 1455 | RHS = conjunct(BPOS,equal(BPOS,TP1,boolean_true(BPOS)),equal(BPOS,TP2,boolean_false(BPOS))), | |
| 1456 | Result = convert_bool(BPOS,disjunct(BPOS,LHS,RHS)). | |
| 1457 | alloy_to_b_boolean_utility_function(FunName, _, BPOS, truth(BPOS)) :- | |
| 1458 | atom_prefix('boolean', FunName), | |
| 1459 | !, | |
| 1460 | add_error(alloy_to_b_boolean_utility_function, 'Function from util/boolean currently not supported', [], BPOS). | |
| 1461 | ||
| 1462 | % dom[r] = dom(r) | |
| 1463 | alloy_to_b_relational_utility_function(UtilFunName, [TRelation], BPOS, TCall) :- | |
| 1464 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1465 | atom_concat(RelationAlias, '\'dom', UtilFunName), | |
| 1466 | !, | |
| 1467 | TCall = domain(BPOS,TRelation). | |
| 1468 | % ran[r] = ran(r) | |
| 1469 | alloy_to_b_relational_utility_function(UtilFunName, [TRelation], BPOS, TCall) :- | |
| 1470 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1471 | atom_concat(RelationAlias, '\'ran', UtilFunName), | |
| 1472 | !, | |
| 1473 | TCall = range(BPOS,TRelation). | |
| 1474 | % total[r,d] = !x.(x:d => r[{x}] /= {}}) | |
| 1475 | alloy_to_b_relational_utility_function(UtilFunName, [TRelation,TDomain], BPOS, TCall) :- | |
| 1476 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1477 | atom_concat(RelationAlias, '\'total', UtilFunName), | |
| 1478 | !, | |
| 1479 | ID0 = identifier(BPOS,x), | |
| 1480 | LHS = member(BPOS,ID0,TDomain), | |
| 1481 | RHS = not_equal(BPOS,image(BPOS,TRelation,set_extension(BPOS,[ID0])),empty_set(BPOS)), | |
| 1482 | TCall = forall(BPOS,[ID0],implication(BPOS,LHS,RHS)). | |
| 1483 | % functional[r,d] = !x.(x:d => card(r[{x}]) <= 1) | |
| 1484 | alloy_to_b_relational_utility_function(UtilFunName, [TRelation,TDomain], BPOS, TCall) :- | |
| 1485 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1486 | atom_concat(RelationAlias, '\'functional', UtilFunName), | |
| 1487 | !, | |
| 1488 | ID0 = identifier(BPOS,x), | |
| 1489 | LHS = member(BPOS,ID0,TDomain), | |
| 1490 | RHS = less_equal(BPOS,card(BPOS,image(BPOS,TRelation,set_extension(BPOS,[ID0]))),integer(BPOS,1)), | |
| 1491 | TCall = forall(BPOS,[ID0],implication(BPOS,LHS,RHS)). | |
| 1492 | % function[r,d] = !x.(x:d => card(r[{x}]) = 1) | |
| 1493 | alloy_to_b_relational_utility_function(UtilFunName, [TRelation,TDomain], BPOS, TCall) :- | |
| 1494 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1495 | atom_concat(RelationAlias, '\'function', UtilFunName), | |
| 1496 | !, | |
| 1497 | ID0 = identifier(BPOS,x), | |
| 1498 | LHS = member(BPOS,ID0,TDomain), | |
| 1499 | RHS = equal(BPOS,card(BPOS,image(BPOS,TRelation,set_extension(BPOS,[ID0]))),integer(BPOS,1)), | |
| 1500 | TCall = forall(BPOS,[ID0],implication(BPOS,LHS,RHS)). | |
| 1501 | % injective[r,c] = !(y).(y:c => card(r~[{y}]) <= 1) | |
| 1502 | alloy_to_b_relational_utility_function(UtilFunName, [TRelation,TCodomain], BPOS, TCall) :- | |
| 1503 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1504 | atom_concat(RelationAlias, '\'injective', UtilFunName), | |
| 1505 | !, | |
| 1506 | ID0 = identifier(BPOS,y), | |
| 1507 | LHS = member(BPOS,ID0,TCodomain), | |
| 1508 | RHS = less_equal(BPOS,card(BPOS,image(BPOS,reverse(BPOS,TRelation),set_extension(BPOS,[ID0]))),integer(BPOS,1)), | |
| 1509 | TCall = forall(BPOS,[ID0],implication(BPOS,LHS,RHS)). | |
| 1510 | % surjective[r,c] = !(y).(y:c => r~[{y}] /= {}) | |
| 1511 | alloy_to_b_relational_utility_function(UtilFunName, [TRelation,TCodomain], BPOS, TCall) :- | |
| 1512 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1513 | atom_concat(RelationAlias, '\'surjective', UtilFunName), | |
| 1514 | !, | |
| 1515 | ID0 = identifier(BPOS,y), | |
| 1516 | LHS = member(BPOS,ID0,TCodomain), | |
| 1517 | RHS = not_equal(BPOS,image(BPOS,reverse(BPOS,TRelation),set_extension(BPOS,[ID0])),empty_set(BPOS)), | |
| 1518 | TCall = forall(BPOS,[ID0],implication(BPOS,LHS,RHS)). | |
| 1519 | % bijective[r,c] = !(y).(y:c => card(r~[{y}]) = 1) | |
| 1520 | alloy_to_b_relational_utility_function(UtilFunName, [TRelation,TCodomain], BPOS, TCall) :- | |
| 1521 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1522 | atom_concat(RelationAlias, '\'bijective', UtilFunName), | |
| 1523 | !, | |
| 1524 | ID0 = identifier(BPOS,y), | |
| 1525 | LHS = member(BPOS,ID0,TCodomain), | |
| 1526 | RHS = equal(BPOS,card(BPOS,image(BPOS,reverse(BPOS,TRelation),set_extension(BPOS,[ID0]))),integer(BPOS,1)), | |
| 1527 | TCall = forall(BPOS,[ID0],implication(BPOS,LHS,RHS)). | |
| 1528 | % bijection[r,d,c] = function[r,d] & bijective[r,c] | |
| 1529 | alloy_to_b_relational_utility_function(UtilFunName, [Relation,Domain,Codomain], BPOS, TCall) :- | |
| 1530 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1531 | atom_concat(RelationAlias, '\'bijection', UtilFunName), | |
| 1532 | !, | |
| 1533 | atom_concat(RelationAlias, '\'function', Function), | |
| 1534 | atom_concat(RelationAlias, '\'bijective', Bijective), | |
| 1535 | alloy_to_b_relational_utility_function(Function, [Relation,Domain], BPOS, IsFunction), | |
| 1536 | alloy_to_b_relational_utility_function(Bijective, [Relation,Codomain], BPOS, IsBijective), | |
| 1537 | TCall = conjunct(BPOS,IsFunction,IsBijective). | |
| 1538 | % reflexive[r,s] = id(s) <: r | |
| 1539 | alloy_to_b_relational_utility_function(UtilFunName, [TRelation1,TRelation2], BPOS, TCall) :- | |
| 1540 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1541 | atom_concat(RelationAlias, '\'reflexive', UtilFunName), | |
| 1542 | !, | |
| 1543 | TCall = subset(BPOS,identity(BPOS,TRelation2),TRelation1). | |
| 1544 | % irreflexive[r] = id(dom(r)) /\ r = {} | |
| 1545 | alloy_to_b_relational_utility_function(UtilFunName, [TRelation], BPOS, TCall) :- | |
| 1546 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1547 | atom_concat(RelationAlias, '\'irreflexive', UtilFunName), | |
| 1548 | !, | |
| 1549 | TCall = equal(BPOS,intersection(BPOS,identity(BPOS,domain(BPOS,TRelation)),TRelation),empty_set(BPOS)). | |
| 1550 | % symmetric[r] = r~ <: r | |
| 1551 | alloy_to_b_relational_utility_function(UtilFunName, [TRelation], BPOS, TCall) :- | |
| 1552 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1553 | atom_concat(RelationAlias, '\'symmetric', UtilFunName), | |
| 1554 | !, | |
| 1555 | TCall = subset(BPOS,reverse(BPOS,TRelation),TRelation). | |
| 1556 | % antisymmetric[r] = (r~ /\ r) <: id(dom(r)) | |
| 1557 | alloy_to_b_relational_utility_function(UtilFunName, [TRelation], BPOS, TCall) :- | |
| 1558 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1559 | atom_concat(RelationAlias, '\'antisymmetric', UtilFunName), | |
| 1560 | !, | |
| 1561 | Intersection = intersection(BPOS,reverse(BPOS,TRelation),TRelation), | |
| 1562 | TCall = subset(BPOS,Intersection,identity(BPOS,domain(BPOS,TRelation))). | |
| 1563 | % transitive[r] = (r ; r) <: r | |
| 1564 | alloy_to_b_relational_utility_function(UtilFunName, [TRelation], BPOS, TCall) :- | |
| 1565 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1566 | atom_concat(RelationAlias, '\'transitive', UtilFunName), | |
| 1567 | !, | |
| 1568 | TCall = subset(BPOS,composition(BPOS,TRelation,TRelation),TRelation). | |
| 1569 | % acyclic[r,s] = !x.(x:s => x|->x /: closure1(r)) | |
| 1570 | alloy_to_b_relational_utility_function(UtilFunName, [TRelation1,TRelation2], BPOS, TCall) :- | |
| 1571 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1572 | atom_concat(RelationAlias, '\'acyclic', UtilFunName), | |
| 1573 | !, | |
| 1574 | ID0 = identifier(BPOS,x), | |
| 1575 | TCall = forall(BPOS,[ID0],implication(BPOS,member(BPOS,ID0,TRelation2), | |
| 1576 | not_member(BPOS,couple(BPOS,ID0,ID0),closure(BPOS,TRelation1)))). | |
| 1577 | % complete[r,s] = !(x,y).(x:s & y:s & x /= y => x|->y : (r \/ r~)) | |
| 1578 | alloy_to_b_relational_utility_function(UtilFunName, [TRelation1,TRelation2], BPOS, TCall) :- | |
| 1579 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1580 | atom_concat(RelationAlias, '\'complete', UtilFunName), | |
| 1581 | !, | |
| 1582 | ID0 = identifier(BPOS,x), | |
| 1583 | ID1 = identifier(BPOS,y), | |
| 1584 | LHS = conjunct(BPOS,conjunct(BPOS,member(BPOS,ID0,TRelation2),member(BPOS,ID1,TRelation2)),not_equal(BPOS,ID0,ID1)), | |
| 1585 | RHS = member(BPOS,couple(BPOS,ID0,ID1),union(BPOS,TRelation1,reverse(BPOS,TRelation1))), | |
| 1586 | TCall = forall(BPOS,[ID0,ID1],implication(BPOS,LHS,RHS)). | |
| 1587 | % preorder[r,s] = reflexive[r,s] & transitive[r] | |
| 1588 | alloy_to_b_relational_utility_function(UtilFunName, [Relation1,Relation2], BPOS, TCall) :- | |
| 1589 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1590 | atom_concat(RelationAlias, '\'preorder', UtilFunName), | |
| 1591 | !, | |
| 1592 | atom_concat(RelationAlias, '\'reflexive', Reflexive), | |
| 1593 | atom_concat(RelationAlias, '\'transitive', Transitive), | |
| 1594 | alloy_to_b_relational_utility_function(Reflexive, [Relation1,Relation2], BPOS, IsReflexive), | |
| 1595 | alloy_to_b_relational_utility_function(Transitive, [Relation1], BPOS, IsTransitive), | |
| 1596 | TCall = conjunct(BPOS,IsReflexive,IsTransitive). | |
| 1597 | % equivalence[r,s] = preorder[r,s] & symmetric[r] | |
| 1598 | alloy_to_b_relational_utility_function(UtilFunName, [Relation1,Relation2], BPOS, TCall) :- | |
| 1599 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1600 | atom_concat(RelationAlias, '\'equivalence', UtilFunName), | |
| 1601 | !, | |
| 1602 | atom_concat(RelationAlias, '\'preorder', Preorder), | |
| 1603 | atom_concat(RelationAlias, '\'symmetric', Symmetric), | |
| 1604 | alloy_to_b_relational_utility_function(Preorder, [Relation1,Relation2], BPOS, IsReflexive), | |
| 1605 | alloy_to_b_relational_utility_function(Symmetric, [Relation1], BPOS, IsTransitive), | |
| 1606 | TCall = conjunct(BPOS,IsReflexive,IsTransitive). | |
| 1607 | % partialOrder[r,s] = preorder[r,s] & antisymmetric[r] | |
| 1608 | alloy_to_b_relational_utility_function(UtilFunName, [Relation1,Relation2], BPOS, TCall) :- | |
| 1609 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1610 | atom_concat(RelationAlias, '\'partialOrder', UtilFunName), | |
| 1611 | !, | |
| 1612 | atom_concat(RelationAlias, '\'preorder', Preorder), | |
| 1613 | atom_concat(RelationAlias, '\'antisymmetric', Antisymmetric), | |
| 1614 | alloy_to_b_relational_utility_function(Preorder, [Relation1,Relation2], BPOS, IsReflexive), | |
| 1615 | alloy_to_b_relational_utility_function(Antisymmetric, [Relation1], BPOS, IsTransitive), | |
| 1616 | TCall = conjunct(BPOS,IsReflexive,IsTransitive). | |
| 1617 | % totalOrder[r,s] = partialOrder[r,s] & complete[r,s] | |
| 1618 | alloy_to_b_relational_utility_function(UtilFunName, [Relation1,Relation2], BPOS, TCall) :- | |
| 1619 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1620 | atom_concat(RelationAlias, '\'totalOrder', UtilFunName), | |
| 1621 | !, | |
| 1622 | atom_concat(RelationAlias, '\'partialOrder', Partialorder), | |
| 1623 | atom_concat(RelationAlias, '\'complete', Complete), | |
| 1624 | alloy_to_b_relational_utility_function(Partialorder, [Relation1,Relation2], BPOS, IsReflexive), | |
| 1625 | alloy_to_b_relational_utility_function(Complete, [Relation1,Relation2], BPOS, IsTransitive), | |
| 1626 | TCall = conjunct(BPOS,IsReflexive,IsTransitive). | |
| 1627 | alloy_to_b_relational_utility_function(FunName, _, BPOS, truth(BPOS)) :- | |
| 1628 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1629 | atom_prefix(RelationAlias, FunName), | |
| 1630 | !, | |
| 1631 | add_error(alloy_to_b_relational_utility_function, 'Function from util/relation currently not supported', [], BPOS). | |
| 1632 | ||
| 1633 | % remove_prime(Old,New) :- atom_codes(Old,OldC) , delete(OldC,39,NewC) , atom_codes(New,NewC). | |
| 1634 | get_clean_ordering_fun_name(OrderingFunctionName, CleanOrdFunName) :- | |
| 1635 | member(CleanOrdFunName, [first,last,min,max,next,nexts,prev,prevs,larger,smaller,lt,lte,gt,gte]), | |
| 1636 | atom_suffix(CleanOrdFunName, OrderingFunctionName). | |
| 1637 | ||
| 1638 | get_ordering_definition_name(TempFunctionName, SignatureName, FunctionName) :- | |
| 1639 | member(TempFunctionName, [next,prev,nexts,prevs]), | |
| 1640 | atom_concat(TempFunctionName, '_', TTempFunctionName), | |
| 1641 | atom_concat(TTempFunctionName, SignatureName, FunctionName). | |
| 1642 | ||
| 1643 | translate_binary_e_p(in(Arg1,Arg2,_Type,POS), Translation) :- | |
| 1644 | !, | |
| 1645 | translate_pos(POS, BPOS), | |
| 1646 | translate_e_p(Arg1, TArg1), | |
| 1647 | translate_binary_in(TArg1, Arg2, BPOS, Translation). | |
| 1648 | translate_binary_e_p(CartTerm, TCartesian) :- | |
| 1649 | is_cartesian_product_term(CartTerm, Arg1, Arg2, POS), | |
| 1650 | !, | |
| 1651 | translate_pos(POS, BPOS), | |
| 1652 | translate_cartesian(BPOS, Arg1, Arg2, TCartesian). | |
| 1653 | % S <: Rel --> {x1,..,xk| x1:S & (x1,...,xk):Rel} | |
| 1654 | translate_binary_e_p(dom_restr(Arg1,Arg2,_Type,POS), TDom) :- | |
| 1655 | \+ is_binary_relation(Arg2), % for binary relation translation to B domain_restriction works | |
| 1656 | !, | |
| 1657 | get_type_and_arity_from_alloy_term(Arg2, _, Arity), | |
| 1658 | gen_ids_and_couple(Arity, IDS, Couple), | |
| 1659 | translate_pos(POS, BPOS), | |
| 1660 | TDom = comprehension_set(BPOS,IDS,conjunct(BPOS,Mem1,Mem2)), | |
| 1661 | IDS = [ID1|_], | |
| 1662 | check_position(BPOS,translate_binary_e_p), | |
| 1663 | Mem1 = member(BPOS,ID1,TArg1), | |
| 1664 | Mem2 = member(BPOS,Couple,TArg2), | |
| 1665 | translate_e_p(Arg1, TArg1), | |
| 1666 | translate_e_p(Arg2, TArg2). | |
| 1667 | translate_binary_e_p(join(Arg1,Arg2,_,_), TJoin) :- | |
| 1668 | % special case for join with unary ordering definition call such as 'this.(prev + next)' | |
| 1669 | % improves performance to translate to 'this.prev + this.next' | |
| 1670 | annotate_undefined_ordering_definition_call(Arg2, Arg1, NArg2), | |
| 1671 | Arg2 \== NArg2, | |
| 1672 | !, | |
| 1673 | translate_e_p(NArg2, TJoin). | |
| 1674 | translate_binary_e_p(join(Arg1,Arg2,_,_), TJoin) :- | |
| 1675 | % see above clause | |
| 1676 | annotate_undefined_ordering_definition_call(Arg1, Arg2, NArg1), | |
| 1677 | Arg1 \== NArg1, | |
| 1678 | !, | |
| 1679 | translate_e_p(NArg1, TJoin). | |
| 1680 | translate_binary_e_p(join(Arg1,Arg2,_Type,POS), TJoin) :- | |
| 1681 | !, | |
| 1682 | translate_pos(POS, BPOS), | |
| 1683 | translate_join(BPOS, Arg1, Arg2, TJoin). | |
| 1684 | translate_binary_e_p(let(VarName,Expr,Sub,Type,POS), TLet) :- | |
| 1685 | !, | |
| 1686 | translate_e_p(VarName, TVarName), | |
| 1687 | translate_e_p(Expr, TExpr), | |
| 1688 | ( Type == type(['PrimitiveBoolean'],0) -> | |
| 1689 | NewFunctor = let_predicate | |
| 1690 | ; NewFunctor = let_expression | |
| 1691 | ), | |
| 1692 | translate_e_p(Sub, TSub), | |
| 1693 | translate_pos(POS, BPOS), | |
| 1694 | TLet =.. [NewFunctor,BPOS,[TVarName],equal(BPOS,TVarName,TExpr),TSub]. | |
| 1695 | translate_binary_e_p(Call, TCall) :- | |
| 1696 | Call =.. [Functor,Name,Params,Type,POS], | |
| 1697 | ( Functor = pred_call | |
| 1698 | ; Functor = fun_call | |
| 1699 | ), | |
| 1700 | !, | |
| 1701 | translate_pos(POS, BPOS), | |
| 1702 | translate_function_call(Name, Params, Type, BPOS, TCall). | |
| 1703 | translate_binary_e_p(Binary, TBinary) :- | |
| 1704 | Binary =.. [Op,Arg1,Arg2,_Type,POS], | |
| 1705 | alloy_to_b_integer_operator(Op, BOp), | |
| 1706 | !, | |
| 1707 | translate_e_p_integer(Arg1, TArg1), | |
| 1708 | translate_e_p_integer(Arg2, TArg2), | |
| 1709 | translate_pos(POS, BPOS), | |
| 1710 | TBinary =.. [BOp,BPOS,TArg1,TArg2]. | |
| 1711 | translate_binary_e_p(Binary, TBinary) :- | |
| 1712 | Binary =.. [Op,Arg1,Arg2,_Type,POS], | |
| 1713 | \+ add_error_for_univ_or_iden(translate_binary_e_p, Op, Arg1, Arg2), | |
| 1714 | alloy_to_b_binary_operator(Op, BOp), | |
| 1715 | translate_e_p(Arg1, TArg1), | |
| 1716 | translate_e_p(Arg2, TArg2), | |
| 1717 | translate_pos(POS, BPOS), | |
| 1718 | TBinary =.. [BOp,BPOS,TArg1,TArg2]. | |
| 1719 | ||
| 1720 | % We do not allow keywords univ or iden for specific operators which we cannot translate to | |
| 1721 | % an equivalent B expression without introducing the universal type. | |
| 1722 | binary_op_not_allowing_iden_or_univ(equal). | |
| 1723 | binary_op_not_allowing_iden_or_univ(not_equal). | |
| 1724 | binary_op_not_allowing_iden_or_univ(in). | |
| 1725 | binary_op_not_allowing_iden_or_univ(not_in). | |
| 1726 | ||
| 1727 | add_error_for_univ_or_iden(Src, Op, Arg1, Arg2) :- | |
| 1728 | binary_op_not_allowing_iden_or_univ(Op), | |
| 1729 | ( ground(Arg1), | |
| 1730 | is_iden(Arg1) | |
| 1731 | ; ground(Arg2), | |
| 1732 | is_iden(Arg2) | |
| 1733 | ), | |
| 1734 | atom_concat('iden keyword in Alloy operator ', Op, Msg), | |
| 1735 | add_error_not_supported(Src, Msg). | |
| 1736 | add_error_for_univ_or_iden(Src, Op, Arg1, Arg2) :- | |
| 1737 | binary_op_not_allowing_iden_or_univ(Op), | |
| 1738 | ( ground(Arg1), | |
| 1739 | is_univ(Arg1) | |
| 1740 | ; ground(Arg2), | |
| 1741 | is_univ(Arg2) | |
| 1742 | ), | |
| 1743 | atom_concat('univ keyword in Alloy operator ', Op, Msg), | |
| 1744 | add_error_not_supported(Src, Msg). | |
| 1745 | ||
| 1746 | add_error_not_supported(Src, NotSupported) :- | |
| 1747 | atom(NotSupported), | |
| 1748 | add_error(Src, 'Expression not supported by our translation: ', [NotSupported]). | |
| 1749 | ||
| 1750 | translate_binary_in(TArg1, Arg2, _, _) :- | |
| 1751 | add_error_for_univ_or_iden(translate_binary_in, in, TArg1, Arg2), | |
| 1752 | !. | |
| 1753 | % translate TArg1 in Arg2 (multplicities are not allowed for not in) | |
| 1754 | translate_binary_in(TArg1, Mult, BPOS, Translation) :- | |
| 1755 | compound(Mult), | |
| 1756 | functor(Mult, AlloyFunctor, 4), % binary operator with type and pos info | |
| 1757 | alloy_to_b_special_multiplicity_type(AlloyFunctor, _, _, _, _, _, _, _), % TO DO: clean up | |
| 1758 | arg(1, Mult, MDom), | |
| 1759 | arg(2, Mult, MRan), | |
| 1760 | translate_e_p(MDom, TMDom), | |
| 1761 | translate_e_p(MRan, TMRan), | |
| 1762 | alloy_to_b_special_multiplicity_type(AlloyFunctor, BPOS, TArg1, TMDom, TMRan, TMult, AdditionalConstraint, UseInverse), | |
| 1763 | !, | |
| 1764 | ( UseInverse == yes | |
| 1765 | -> TTArg1 = reverse(BPOS,TArg1) | |
| 1766 | ; TTArg1 = TArg1 | |
| 1767 | ), | |
| 1768 | ( AdditionalConstraint == none | |
| 1769 | -> Translation = member(BPOS,TTArg1,TMult) % use element of rather than subset for special type operators | |
| 1770 | ; Translation = conjunct(BPOS,member(BPOS,TTArg1,TMult),AdditionalConstraint) | |
| 1771 | ). | |
| 1772 | % cartesian | |
| 1773 | translate_binary_in(TArg1, Arg2, BPOS, subset(BPOS,TArg1,TArg2)) :- | |
| 1774 | translate_e_p(Arg2, TArg2). | |
| 1775 | ||
| 1776 | % translate expressions of the form Arg1 MULT -> MULT Arg2 with MULT : {some,lone, one, ''} | |
| 1777 | % The result is to be used in member(Pos,LHS,TBinary) not for subset checks ! | |
| 1778 | translate_special_field_multiplicity_binary_e_p(Binary, TBinary) :- | |
| 1779 | Binary =.. [AlloyFunctor,Arg1,Arg2,_Type,POS], | |
| 1780 | translate_pos(POS, BPOS), | |
| 1781 | translate_e_p(Arg1, TArg1), | |
| 1782 | translate_e_p(Arg2, TArg2), | |
| 1783 | % some functions of alloy_to_b_special_multiplicity_type/8 do not apply to | |
| 1784 | % field multiplicities as only one multiplicity is allowed there | |
| 1785 | alloy_to_b_special_multiplicity_type(AlloyFunctor, BPOS, _, TArg1, TArg2, TBinary, _, _WasNo). | |
| 1786 | ||
| 1787 | % Alloy: r in T -> some U | |
| 1788 | % B: r : T <-> U & dom(r)=T | |
| 1789 | alloy_to_b_special_multiplicity_type(total_relation, BPOS, TRel, TMDom, TMRan, relations(BPOS,TMDom,TMRan), AdditionalConstraint, no) :- | |
| 1790 | AdditionalConstraint = equal(BPOS,domain(BPOS,TRel),TMDom). | |
| 1791 | % Alloy: r in T -> one U | |
| 1792 | % B: r : T --> U | |
| 1793 | alloy_to_b_special_multiplicity_type(total_function, BPOS, _, TMDom, TMRan, total_function(BPOS,TMDom,TMRan), none, no). | |
| 1794 | % Alloy: r in T -> lone U | |
| 1795 | % B: r : T +-> U | |
| 1796 | alloy_to_b_special_multiplicity_type(partial_function, BPOS, _, TMDom, TMRan, partial_function(BPOS,TMDom,TMRan), none, no). | |
| 1797 | % Alloy: r in T some -> U | |
| 1798 | % B: r : T <-> U & ran(r) = U | |
| 1799 | alloy_to_b_special_multiplicity_type(surjection_relation, BPOS, TRel, TMDom, TMRan, relations(BPOS,TMDom,TMRan), AdditionalConstraint, no) :- | |
| 1800 | AdditionalConstraint = equal(BPOS,range(BPOS,TRel),TMRan). | |
| 1801 | % Alloy: r in T some -> some U | |
| 1802 | % B: r : T <-> U & dom(r)=T & ran(r) = U | |
| 1803 | alloy_to_b_special_multiplicity_type(total_surjection_relation, BPOS, TRel, TMDom, TMRan, relations(BPOS,TMDom,TMRan), AdditionalConstraint, no) :- | |
| 1804 | AdditionalConstraint = conjunct(BPOS,equal(BPOS,domain(BPOS,TRel),TMDom),equal(BPOS,range(BPOS,TRel),TMRan)). | |
| 1805 | % Alloy: r in T some -> lone U | |
| 1806 | % B: r : T +->> U | |
| 1807 | alloy_to_b_special_multiplicity_type(partial_surjection, BPOS, _, TMDom, TMRan, partial_surjection(BPOS,TMDom,TMRan), none, no). | |
| 1808 | % Alloy: r in T some -> one U | |
| 1809 | % B: r : T -->> U | |
| 1810 | alloy_to_b_special_multiplicity_type(total_surjection, BPOS, _, TMDom, TMRan, total_surjection(BPOS,TMDom,TMRan), none, no). | |
| 1811 | % Alloy: r in T lone -> U | |
| 1812 | % B: r~ : U +-> T | |
| 1813 | alloy_to_b_special_multiplicity_type(injection_relation, BPOS, _, TMDom, TMRan, partial_function(BPOS,TMRan,TMDom), none, yes). | |
| 1814 | % Alloy: r in T lone -> some U | |
| 1815 | % B: r~ : U +->> T | |
| 1816 | alloy_to_b_special_multiplicity_type(injection_surjection_relation, BPOS, _, TMDom, TMRan, partial_surjection(BPOS,TMRan,TMDom), none, yes). | |
| 1817 | % Alloy: r in T lone -> lone U | |
| 1818 | % B: r : T >+> U | |
| 1819 | alloy_to_b_special_multiplicity_type(partial_injection, BPOS, _, TMDom, TMRan, partial_injection(BPOS,TMDom,TMRan), none, no). | |
| 1820 | % Alloy: r in T lone -> one U | |
| 1821 | % B: r : T >-> U | |
| 1822 | alloy_to_b_special_multiplicity_type(total_injection, BPOS, _, TMDom, TMRan, total_injection(BPOS,TMDom,TMRan), none, no). | |
| 1823 | % Alloy: r in T one -> U | |
| 1824 | % B: r~ : U --> T | |
| 1825 | alloy_to_b_special_multiplicity_type(bijection_relation, BPOS, _, TMDom, TMRan, total_function(BPOS,TMRan,TMDom), none, yes). | |
| 1826 | % Alloy: r in T one -> some U | |
| 1827 | % B: r~ : U -->> T | |
| 1828 | alloy_to_b_special_multiplicity_type(total_bijection_relation, BPOS, _, TMDom, TMRan, total_surjection(BPOS,TMRan,TMDom), none, yes). | |
| 1829 | % Alloy: r in T one -> lone U | |
| 1830 | % B: r : T >+>> U | |
| 1831 | alloy_to_b_special_multiplicity_type(partial_bijection, BPOS, _, TMDom, TMRan, partial_bijection(BPOS,TMDom,TMRan), none, no). | |
| 1832 | % Alloy: r in T one -> one U | |
| 1833 | % B: r : T >->> U | |
| 1834 | alloy_to_b_special_multiplicity_type(total_bijection, BPOS, _, TMDom, TMRan, total_bijection(BPOS,TMDom,TMRan), none, no). | |
| 1835 | ||
| 1836 | % Note: Sequences in B are indexed from 1 to n, in Alloy from 0 to n-1. | |
| 1837 | % We do not use B sequences when translating from Alloy but define a partial function with domain 0..n-1 | |
| 1838 | % (we have to manually implement most functions anyway) | |
| 1839 | % Documentation available at http://alloytools.org/quickguide/seq.html | |
| 1840 | %% Sequence function calls without a parameter but the sequence itself. | |
| 1841 | % first: seq[{0}] | |
| 1842 | sequence_function_to_b('seq\'first', BPOS, [Seq], image(BPOS,Seq,set_extension(BPOS,[integer(BPOS,0)]))). | |
| 1843 | % last: seq[{card(seq)-1}] | |
| 1844 | sequence_function_to_b('seq\'last', BPOS, [Seq], image(BPOS,Seq,set_extension(BPOS,[minus(BPOS,card(BPOS,Seq),integer(BPOS,1))]))). | |
| 1845 | % rest: IF seq = <> THEN <> ELSE %x.(x:0..card(seq)-2 | seq(x+1) END | |
| 1846 | sequence_function_to_b('seq\'rest', BPOS, [Seq], if_then_else(BPOS,equal(BPOS,Seq,empty_sequence(BPOS)),empty_sequence(BPOS),lambda(BPOS,[identifier(BPOS,x)],member(BPOS,identifier(BPOS,x),interval(BPOS,integer(BPOS,0),minus(BPOS,card(BPOS,Seq),integer(BPOS,2)))),function(BPOS,Seq,add(BPOS,identifier(BPOS,x),integer(BPOS,1)))))). | |
| 1847 | % elems: ran(seq) | |
| 1848 | sequence_function_to_b('seq\'elems', BPOS, [Seq], range(BPOS,Seq)). | |
| 1849 | % butlast: seq[{card(seq)-2}] | |
| 1850 | sequence_function_to_b('seq\'butlast', BPOS, [Seq], image(BPOS,Seq,set_extension(BPOS,[minus(BPOS,card(BPOS,Seq),integer(BPOS,2))]))). | |
| 1851 | % isEmpty: seq = <> | |
| 1852 | sequence_function_to_b('seq\'isEmpty', BPOS, [Seq], equal(BPOS,Seq,empty_sequence(BPOS))). | |
| 1853 | % hasDups: card(seq) /= card(ran(seq)) | |
| 1854 | sequence_function_to_b('seq\'hasDups', BPOS, [Seq], not_equal(BPOS,card(BPOS,Seq),card(BPOS,range(BPOS,Seq)))). | |
| 1855 | % inds: 0..card(seq)-1 | |
| 1856 | sequence_function_to_b('seq\'inds', BPOS, [Seq], interval(BPOS,integer(BPOS,0),minus(BPOS,card(BPOS,Seq),integer(BPOS,1)))). | |
| 1857 | % lastIdx: {card(seq)-1} /\ 0..(card(seq)-1) | |
| 1858 | sequence_function_to_b('seq\'lastIdx', BPOS, [Seq], intersection(BPOS,set_extension(BPOS,[minus(BPOS,card(BPOS,Seq),integer(BPOS,1))]),interval(BPOS,integer(BPOS,0),minus(BPOS,card(BPOS,Seq),integer(BPOS,1))))). | |
| 1859 | % afterLastIdx: {card(seq)} /\ 0..(MAXSEQ-1) | |
| 1860 | sequence_function_to_b('seq\'afterLastIdx', BPOS, [Seq], intersection(BPOS,set_extension(BPOS,[card(BPOS,Seq)]),interval(BPOS,integer(BPOS,0),minus(BPOS,integer(BPOS,MaxSeq),integer(BPOS,1))))) :- | |
| 1861 | maxseq(MaxSeq). | |
| 1862 | %% Sequence function calls with one parameter and the sequence itself. | |
| 1863 | % idxOf[X]: IF seq~[{E_{one}(X)}] /= {} THEN {min(seq~[{E_{one}(X)}])} ELSE {} END | |
| 1864 | sequence_function_to_b('seq\'idxOf', BPOS, [Seq,P1], if_then_else(BPOS,not_equal(BPOS,image(BPOS,reverse(BPOS,Seq),set_extension(BPOS,[P1One])),empty_set(BPOS)),set_extension(BPOS,[min(BPOS,image(BPOS,reverse(BPOS,Seq),set_extension(BPOS,[P1One])))]),empty_set(BPOS))) :- | |
| 1865 | translate_e_p_one(P1, P1One). | |
| 1866 | % lastIdxOf[X]: IF seq~[{E_{one}(X)}] /= {} THEN {max(seq~[{E_{one}(X)}])} ELSE {} END | |
| 1867 | sequence_function_to_b('seq\'lastIdxOf', BPOS, [Seq,P1], if_then_else(BPOS,not_equal(BPOS,image(BPOS,reverse(BPOS,Seq),set_extension(BPOS,[P1One])),empty_set(BPOS)),set_extension(BPOS,[max(BPOS,image(BPOS,reverse(BPOS,Seq),set_extension(BPOS,[P1One])))]),empty_set(BPOS))) :- | |
| 1868 | translate_e_p_one(P1, P1One). | |
| 1869 | % indsOf[X]: seq~[{E_{one}(X)}] | |
| 1870 | sequence_function_to_b('seq\'indsOf', BPOS, [Seq,P1], image(BPOS,reverse(BPOS,Seq),set_extension(BPOS,[P1One]))) :- | |
| 1871 | translate_e_p_one(P1, P1One). | |
| 1872 | % append[seq2]: (0..(MAXSEQ-1)) <| (seq \/ %x.(x:card(seq)..(card(seq)+card(seq2)-1) | seq2(x-card(seq)))) | |
| 1873 | sequence_function_to_b('seq\'append', BPOS, [Seq,P1], domain_restriction(BPOS,interval(BPOS,integer(BPOS,0),minus(BPOS,integer(BPOS,MaxSeq),integer(BPOS,1))),union(BPOS,Seq,lambda(BPOS,[identifier(BPOS,x)],member(BPOS,identifier(BPOS,x),interval(BPOS,card(BPOS,Seq),minus(BPOS,add(BPOS,card(BPOS,Seq),card(BPOS,P1)),integer(BPOS,1)))),function(BPOS,P1,minus(BPOS,identifier(BPOS,x),card(BPOS,Seq))))))) :- | |
| 1874 | maxseq(MaxSeq). | |
| 1875 | % Throw WD error if X is not singleton. | |
| 1876 | % add[X]: IF card(seq) < MAXSEQ THEN seq \/ {card(seq) |-> E_{one}(X)} ELSE seq END | |
| 1877 | sequence_function_to_b('seq\'add', BPOS, [Seq,P1], if_then_else(BPOS,less(BPOS,card(BPOS,Seq),integer(BPOS,MaxSeq)),union(BPOS,Seq,set_extension(BPOS,[couple(BPOS,card(BPOS,Seq),P1One)])),Seq)) :- | |
| 1878 | maxseq(MaxSeq), | |
| 1879 | translate_e_p_one(P1, P1One). | |
| 1880 | % delete[i]: IF (i >= 0) THEN (0..(i-1) <| seq) \/ %x.(x:i..(card(seq)-2) & (x+1):dom(seq) | seq(x+1)) ELSE seq END | |
| 1881 | sequence_function_to_b('seq\'delete', BPOS, [Seq,P1], if_then_else(BPOS,greater_equal(BPOS,P1Int,integer(BPOS,0)),union(BPOS,domain_restriction(BPOS,interval(BPOS,integer(BPOS,0),minus(BPOS,P1Int,integer(BPOS,1))),Seq),lambda(BPOS,[identifier(BPOS,x)],conjunct(BPOS,member(BPOS,identifier(BPOS,x),interval(BPOS,P1Int,minus(BPOS,card(BPOS,Seq),integer(BPOS,2)))),member(BPOS,add(BPOS,identifier(BPOS,x),integer(BPOS,1)),domain(BPOS,Seq))),function(BPOS,Seq,add(BPOS,identifier(BPOS,x),integer(BPOS,1))))),Seq)) :- | |
| 1882 | untyped_b_ast_to_integer(P1, P1Int). | |
| 1883 | % Throw WD error if X is not singleton. | |
| 1884 | % setAt[i,X]: IF (i >= 0 & i <= card(seq) ) THEN seq <+ {i |-> E_{one}(X)} ELSE seq END | |
| 1885 | sequence_function_to_b('seq\'setAt', BPOS, [Seq,P1,P2], if_then_else(BPOS,conjunct(BPOS,greater_equal(BPOS,P1Int,integer(BPOS,0)),less_equal(BPOS,P1Int,card(BPOS,Seq))),overwrite(Seq,set_extension(BPOS,[couple(BPOS,P1Int,P2One)])),Seq)) :- | |
| 1886 | untyped_b_ast_to_integer(P1, P1Int), | |
| 1887 | translate_e_p_one(P2, P2One). | |
| 1888 | % Throw WD error if X is not singleton. | |
| 1889 | % special case for i=0 | |
| 1890 | % insert[0,X]: 0..(m-1) <| {0 |-> E_{one}(X)} \/ %z.(z:1..card(seq) ∧ (z-1):dom(seq) | seq(z-1))) | |
| 1891 | sequence_function_to_b('seq\'insert', BPOS, [Seq,P1,P2], domain_restriction(BPOS,interval(BPOS,integer(BPOS,0),minus(BPOS,integer(BPOS,MaxSeq),integer(BPOS,1))),union(BPOS,set_extension(BPOS,[couple(BPOS,integer(BPOS,0),P2One)]),lambda(BPOS,[identifier(BPOS,z)],member(BPOS,identifier(BPOS,z),interval(BPOS,integer(BPOS,1),card(BPOS,Seq))),function(BPOS,Seq,minus(BPOS,identifier(BPOS,z),integer(BPOS,1))))))) :- | |
| 1892 | untyped_b_ast_to_integer(P1, P1Int), | |
| 1893 | P1Int = integer(_,0), | |
| 1894 | maxseq(MaxSeq), | |
| 1895 | translate_e_p_one(P2, P2One). | |
| 1896 | % insert[i,X]: 0..(m-1) <| ((0..(i-1) <| seq) \/ {i |-> E_{one}(X)} \/ %z.(z:(i+1)..card(seq) ∧ (z-1):dom(seq) | seq(z-1))) | |
| 1897 | sequence_function_to_b('seq\'insert', BPOS, [Seq,P1,P2], domain_restriction(BPOS,interval(BPOS,integer(BPOS,0),minus(BPOS,integer(BPOS,MaxSeq),integer(BPOS,1))),union(BPOS,union(BPOS,domain_restriction(BPOS,interval(BPOS,integer(BPOS,0),minus(BPOS,P1Int,integer(BPOS,1))),Seq),set_extension(BPOS,[couple(BPOS,P1Int,P2One)])),lambda(BPOS,[identifier(BPOS,z)],member(BPOS,identifier(BPOS,z),interval(BPOS,add(BPOS,P1Int,integer(BPOS,1)),card(BPOS,Seq))),function(BPOS,Seq,minus(BPOS,identifier(BPOS,z),integer(BPOS,1))))))) :- | |
| 1898 | P1 \= integer(_,0), | |
| 1899 | maxseq(MaxSeq), | |
| 1900 | untyped_b_ast_to_integer(P1, P1Int), | |
| 1901 | translate_e_p_one(P2, P2One). | |
| 1902 | % subseq[from,to]: IF 0 <= from & from <= to & to < card(seq) THEN %z.(z:0..(to-from) & (z+from):dom(seq) | seq(z+from)) ELSE {} END | |
| 1903 | sequence_function_to_b('seq\'subseq', BPOS, [Seq,P1,P2], if_then_else(BPOS,conjunct(BPOS,conjunct(BPOS,less_equal(BPOS,integer(BPOS,0),P1Int),less_equal(BPOS,P1Int,P2Int)),less(BPOS,P2Int,card(BPOS,Seq))),lambda(BPOS,[identifier(BPOS,z)],member(BPOS,identifier(BPOS,z),interval(BPOS,integer(BPOS,0),minus(BPOS,P2Int,P1Int))),function(BPOS,Seq,add(BPOS,identifier(BPOS,z),P1Int))),empty_set(BPOS))) :- | |
| 1904 | untyped_b_ast_to_integer(P1, P1Int), | |
| 1905 | untyped_b_ast_to_integer(P2, P2Int). | |
| 1906 | sequence_function_to_b(FunName, BPOS, _, Res) :- | |
| 1907 | atom_prefix('seq', FunName), | |
| 1908 | !, | |
| 1909 | add_error(sequence_function_to_b, 'Function from util/sequences currently not supported', [], BPOS), | |
| 1910 | Res = truth(BPOS). | |
| 1911 | ||
| 1912 | translate_seq_function_param(join(identifier(this,type([Type],1),IPos),Arg2,JType,JPos), TParam) :- | |
| 1913 | !, | |
| 1914 | % remove join with this for signature fields | |
| 1915 | translate_e_p(join(identifier(Type,type([Type],1),IPos),Arg2,JType,JPos), TTParam), | |
| 1916 | TParam = TTParam. | |
| 1917 | translate_seq_function_param(Param, TParam) :- | |
| 1918 | translate_e_p(Param, TParam). | |
| 1919 | ||
| 1920 | % Translation of operations from utility libraries | |
| 1921 | % util/sequence | |
| 1922 | translate_function_call(Function, Params, _Type, BPOS, TCall) :- | |
| 1923 | maplist(translate_seq_function_param, Params, TParams), | |
| 1924 | sequence_function_to_b(Function, BPOS, TParams, TCall), | |
| 1925 | !. | |
| 1926 | % util/boolean | |
| 1927 | translate_function_call(Name, Params, _Type, BPOS, Result) :- | |
| 1928 | maplist(translate_e_p, Params, TParams), | |
| 1929 | alloy_to_b_boolean_utility_function(Name, TParams, BPOS, Result). | |
| 1930 | % util/relation | |
| 1931 | translate_function_call(Name, Params, _Type, BPOS, Result) :- | |
| 1932 | maplist(translate_e_p, Params, TParams), | |
| 1933 | check_position(BPOS,alloy_to_b_relational_utility_function), | |
| 1934 | alloy_to_b_relational_utility_function(Name, TParams, BPOS, Result). | |
| 1935 | % util/integer with no direct counterparts in B | |
| 1936 | translate_function_call(Name, Params, _Type, BPOS, Result) :- | |
| 1937 | is_util_integer_natural_func(Name, UtilType, AlloyOp), | |
| 1938 | UtilType == integer, | |
| 1939 | maplist(translate_e_p_integer, Params, TParams), | |
| 1940 | alloy_to_b_integer_utility_function(AlloyOp, BPOS, TParams, Result). | |
| 1941 | % util/natural with no direct counterparts in B | |
| 1942 | translate_function_call(Name, Params, _Type, BPOS, Result) :- | |
| 1943 | is_util_integer_natural_func(Name, UtilType, AlloyOp), | |
| 1944 | UtilType == natural, | |
| 1945 | maplist(translate_e_p_integer, Params, TParams), | |
| 1946 | alloy_to_b_natural_utility_function(AlloyOp, BPOS, TParams, Result), | |
| 1947 | !. | |
| 1948 | % util/integer and util/natural with direct counterparts in B | |
| 1949 | translate_function_call(Name, Params, _Type, BPOS, Result) :- | |
| 1950 | length(Params, Arity), | |
| 1951 | alloy_to_b_integer_natural_utility_func(Name, Arity, BOp, ArgType, ReturnType), | |
| 1952 | !, % functions like plus, minus, mul, ... with integer arguments and result | |
| 1953 | ( ArgType = integer -> | |
| 1954 | maplist(translate_e_p_integer, Params, TParams) | |
| 1955 | ; maplist(translate_e_p, Params, TParams) | |
| 1956 | ), | |
| 1957 | ( ReturnType = integer -> | |
| 1958 | Result = set_extension(BPOS,[TCall]) % we add set_extension wrapper | |
| 1959 | ; Result = TCall | |
| 1960 | ), | |
| 1961 | TCall =.. [BOp,BPOS|TParams]. | |
| 1962 | % util/ordering | |
| 1963 | translate_function_call(FunName, Params, type([SignatureName|_],_), BPOS, TCall) :- | |
| 1964 | translate_e_p(SignatureName, TSignatureName), | |
| 1965 | get_clean_ordering_fun_name(FunName, CleanOrdFunName), | |
| 1966 | translate_ordering_function(CleanOrdFunName, Params, SignatureName, TSignatureName, BPOS, TCall). | |
| 1967 | % definition call for calls to user defined Alloy predicates and functions | |
| 1968 | translate_function_call(Name, Params, _, BPOS, TCall) :- | |
| 1969 | % predicate and function call | |
| 1970 | maplist(translate_e_p, Params, TParams), | |
| 1971 | ( (definition_without_param(Name), TParams = [TParam]) | |
| 1972 | -> TCall = image(BPOS,definition(BPOS,Name,[]),TParam) | |
| 1973 | ; maplist(strip_singleton_set_from_this, TParams, TTParams), % identifier 'this' is added for fields which is already wrapped in a set extension | |
| 1974 | TCall = definition(BPOS,Name,TTParams) | |
| 1975 | ). | |
| 1976 | ||
| 1977 | % first: IF S_ord /= {} THEN {min(S_ord)} ELSE {} | |
| 1978 | 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))) :- | |
| 1979 | !. | |
| 1980 | % last: IF S_ord /= {} THEN {max(S_ord)} ELSE {} | |
| 1981 | 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))) :- | |
| 1982 | !. | |
| 1983 | % min[p]: IF p /= {} THEN {min(p)} ELSE {} | |
| 1984 | % max[p]: IF p /= {} THEN {min(p)} ELSE {} | |
| 1985 | translate_ordering_function(FunName, [Param], _, _, BPOS, TCall) :- | |
| 1986 | ( FunName == min | |
| 1987 | ; FunName == max | |
| 1988 | ), | |
| 1989 | !, | |
| 1990 | translate_e_p(Param, TParam), | |
| 1991 | InnerCall =.. [FunName,BPOS,TParam], | |
| 1992 | TCall = if_then_else(BPOS,not_equal(BPOS,TParam,empty_set(BPOS)),set_extension(BPOS,[InnerCall]),empty_set(BPOS)). | |
| 1993 | translate_ordering_function(FunName, [TParam], SignatureName, _, BPOS, TCall) :- | |
| 1994 | ( FunName == next | |
| 1995 | ; FunName == nexts | |
| 1996 | ; FunName == prev | |
| 1997 | ; FunName == prevs | |
| 1998 | ), | |
| 1999 | !, | |
| 2000 | get_ordering_definition_name(FunName, SignatureName, DefName), | |
| 2001 | translate_e_p(TParam, TTParam), | |
| 2002 | strip_singleton_set_from_this(TTParam, Param), | |
| 2003 | % The definition is something like this: next_House(s) == IF succ()[s] <: House THEN succ()[s] ELSE {} END | |
| 2004 | TCall = definition(BPOS,DefName,[Param]). | |
| 2005 | % larger[p1,p1]: IF p1 \/ p2 /= {} THEN {max(p1 \/ p2)} ELSE {} END | |
| 2006 | % smaller[p1,p2]: IF p1 \/ p2 /= {} THEN {min(p1 \/ p2)} ELSE {} END | |
| 2007 | translate_ordering_function(FunName, [P1,P2], _, _, BPOS, TCall) :- | |
| 2008 | ( FunName == larger | |
| 2009 | ; FunName == smaller | |
| 2010 | ), | |
| 2011 | !, | |
| 2012 | get_partial_b_functor_for_ordering(FunName, BFunctor), | |
| 2013 | translate_e_p(P1, TP1), | |
| 2014 | translate_e_p(P2, TP2), | |
| 2015 | ParamUnion = union(BPOS,TP1,TP2), | |
| 2016 | TInnerCall =.. [BFunctor,BPOS,ParamUnion], | |
| 2017 | InnerCall = set_extension(BPOS,[TInnerCall]), | |
| 2018 | TCall = if_then_else(BPOS,not_equal(BPOS,ParamUnion,empty_set(BPOS)),InnerCall,empty_set(BPOS)). | |
| 2019 | % lt[p1,p2]: (p1 = {}) or (p1 /= {} & p2 /= {} & p1 /= p2 & {min(p1 \/ p2)} = p1)) | |
| 2020 | % gt[p1,p2]: (p1 = {}) or (p1 /= {} & p2 /= {} & p1 /= p2 & {max(p1 \/ p2)} = p1)) | |
| 2021 | translate_ordering_function(FunName, [P1,P2], _, _, BPOS, TCall) :- | |
| 2022 | ( FunName == lt | |
| 2023 | ; FunName == gt | |
| 2024 | ), | |
| 2025 | !, | |
| 2026 | get_partial_b_functor_for_ordering(FunName, BFunctor), | |
| 2027 | translate_e_p(P1, TP1), | |
| 2028 | translate_e_p(P2, TP2), | |
| 2029 | TInnerCall =.. [BFunctor,BPOS,union(BPOS,TP1,TP2)], | |
| 2030 | InnerCall = set_extension(BPOS,[TInnerCall]), | |
| 2031 | LHS = equal(BPOS,TP1,empty_set(BPOS)), | |
| 2032 | RHS = conjunct(BPOS,conjunct(BPOS,conjunct(BPOS,not_equal(BPOS,TP1,empty_set(BPOS)), | |
| 2033 | not_equal(BPOS,TP2,empty_set(BPOS))), | |
| 2034 | not_equal(BPOS,TP1,TP2)), | |
| 2035 | equal(BPOS,InnerCall,TP1)), | |
| 2036 | TCall = disjunct(BPOS,LHS,RHS). | |
| 2037 | % lte[p1,p2]: (p1 = {}) or (p1 /= {} & p2 /= {} & {min(p1 \/ p2)} = p1) | |
| 2038 | % gte[p1,p2]: (p1 = {}) or (p1 /= {} & p2 /= {} & {max(p1 \/ p2)} = p1) | |
| 2039 | translate_ordering_function(FunName, [P1,P2], _, _, BPOS, TCall) :- | |
| 2040 | ( FunName == lte | |
| 2041 | ; FunName == gte | |
| 2042 | ), | |
| 2043 | !, | |
| 2044 | get_partial_b_functor_for_ordering(FunName, BFunctor), | |
| 2045 | translate_e_p(P1, TP1), | |
| 2046 | translate_e_p(P2, TP2), | |
| 2047 | TInnerCall =.. [BFunctor,BPOS,union(BPOS,TP1,TP2)], | |
| 2048 | InnerCall = set_extension(BPOS,[TInnerCall]), | |
| 2049 | LHS = equal(BPOS,TP1,empty_set(BPOS)), | |
| 2050 | RHS = conjunct(BPOS,conjunct(BPOS,not_equal(BPOS,TP1,empty_set(BPOS)), | |
| 2051 | not_equal(BPOS,TP2,empty_set(BPOS))), | |
| 2052 | equal(BPOS,InnerCall,TP1)), | |
| 2053 | TCall = disjunct(BPOS,LHS,RHS). | |
| 2054 | translate_ordering_function(FunName, [], SignatureName, _, BPOS, Res) :- | |
| 2055 | % ordering without argument used in a unary operator, e.g., 'some t : Trace | all s : t.^next | s.state = Off' | |
| 2056 | % as used in reset_flip_flop_with_enable.als | |
| 2057 | % for binary operators, we can inline joins as is done in annotate_undefined_ordering_definition_call/3 | |
| 2058 | ( FunName == next | |
| 2059 | ; FunName == nexts | |
| 2060 | ; FunName == prev | |
| 2061 | ; FunName == prevs | |
| 2062 | ), | |
| 2063 | !, | |
| 2064 | get_ordering_definition_name(FunName, SignatureName, DefName), | |
| 2065 | % e.g., generate %x.(x:House|MU(next_House({x}))) | |
| 2066 | TCall = mu(BPOS,definition(BPOS,DefName,[TParam])), | |
| 2067 | TId = identifier(BPOS,'_o_0'), | |
| 2068 | TParam = set_extension(BPOS,[TId]), | |
| 2069 | Member = member(BPOS,TId,identifier(BPOS,SignatureName)), | |
| 2070 | Res = lambda(BPOS,[TId],Member,TCall). | |
| 2071 | translate_ordering_function(FunName, Params, SignatureName, _Type, BPOS, empty_set(BPOS)) :- | |
| 2072 | length(Params,Arity), | |
| 2073 | ajoin(['Cannot translate ordering function for ',SignatureName,':'],Msg), | |
| 2074 | add_error(translate_ordering_function, Msg, FunName/Arity, BPOS). | |
| 2075 | ||
| 2076 | get_partial_b_functor_for_ordering(larger, max). | |
| 2077 | get_partial_b_functor_for_ordering(smaller, min). | |
| 2078 | get_partial_b_functor_for_ordering(lt, min). | |
| 2079 | get_partial_b_functor_for_ordering(lte, min). | |
| 2080 | get_partial_b_functor_for_ordering(gt, max). | |
| 2081 | get_partial_b_functor_for_ordering(gte, max). | |
| 2082 | ||
| 2083 | strip_singleton_set(set_extension(_,[identifier(Pos,Name)]), identifier(Pos,Name)) :- | |
| 2084 | !. | |
| 2085 | strip_singleton_set(A, A). | |
| 2086 | ||
| 2087 | strip_singleton_set_from_this(set_extension(_,[identifier(Pos,this)]), identifier(Pos,this)) :- | |
| 2088 | !. | |
| 2089 | strip_singleton_set_from_this(A, A). | |
| 2090 | ||
| 2091 | translate_cartesian(TPos, Arg1, Arg2, Res) :- | |
| 2092 | translate_e_p(Arg1, TArg1), | |
| 2093 | translate_cartesian2(TPos, TArg1, Arg2, Res). | |
| 2094 | ||
| 2095 | translate_cartesian2(TPos, TArg1, Arg2, Res) :- | |
| 2096 | translate_e_p(Arg2, TArg2), | |
| 2097 | translate_cartesian3(TPos, TArg1, Arg2, TArg2, Res). | |
| 2098 | % P -> Q --> P*Q | |
| 2099 | translate_cartesian3(TPos, TArg1, Arg2, TArg2, cartesian_product(TPos,TArg1,TArg2)) :- | |
| 2100 | is_unary_relation(Arg2), | |
| 2101 | !. | |
| 2102 | % P -> Q --> {c0, c1,...,ck | c0:P & (c1,...,ck):Q} | |
| 2103 | translate_cartesian3(TPos, TArg1, Arg2, TArg2, comprehension_set(TPos,[ID0|IDs2],conjunct(TPos,Mem1,Mem2))) :- | |
| 2104 | get_type_and_arity_from_alloy_term(Arg2, _Type, Arity), | |
| 2105 | gen_ids_and_couple(Arity, IDs2, Couple2), | |
| 2106 | gen_identifier(0, "_c_", ID0), | |
| 2107 | check_position(TPos,translate_cartesian3), | |
| 2108 | Mem1 = member(TPos,ID0,TArg1), | |
| 2109 | Mem2 = member(TPos,Couple2,TArg2). | |
| 2110 | ||
| 2111 | gen_ids_and_couple(Arity, [ID1|IDListRest], NestedCouple) :- | |
| 2112 | Arity > 0, | |
| 2113 | gen_identifier(1, "_c_", ID1), | |
| 2114 | gen_ids_and_couple(2, Arity, IDListRest, ID1, NestedCouple). | |
| 2115 | ||
| 2116 | gen_ids_and_couple(Nr, Arity, L, Acc, Res) :- | |
| 2117 | Nr > Arity, | |
| 2118 | !, | |
| 2119 | L = [], | |
| 2120 | Res = Acc. | |
| 2121 | gen_ids_and_couple(Nr, Arity, [IDN|T], Acc, Res) :- | |
| 2122 | gen_identifier(Nr, "_c_", IDN), | |
| 2123 | N1 is Nr+1, | |
| 2124 | gen_ids_and_couple(N1, Arity, T, couple(none,Acc,IDN), Res). | |
| 2125 | ||
| 2126 | gen_identifier(Nr, Prefix, identifier(none,ID)) :- | |
| 2127 | number_codes(Nr, NrC), | |
| 2128 | append(Prefix, NrC, AC), | |
| 2129 | atom_codes(ID, AC). | |
| 2130 | ||
| 2131 | is_ordering_definition_call(FunCall) :- | |
| 2132 | FunCall =.. [Functor,Name,_,_,_], | |
| 2133 | Functor == fun_call, | |
| 2134 | atom_concat('ordering\'', Rest, Name), | |
| 2135 | memberchk(Rest, [next,prev,nexts,prevs]). | |
| 2136 | ||
| 2137 | %% annotate_undefined_ordering_definition_call(+AlloyTerm, +AnnotateWith, -AnnotatedAlloyTerm). | |
| 2138 | % Top-level call is assumed to be a join. We join "undefined" ordering definition calls in | |
| 2139 | % arguments of the top-level join with an Alloy term. | |
| 2140 | % For instance: | |
| 2141 | % 'this.(prev + next)', where it actually is 'this.prev + this.next' as used in einsteins_enum.als | |
| 2142 | annotate_undefined_ordering_definition_call(Atom, _, Out) :- | |
| 2143 | atom(Atom), | |
| 2144 | !, | |
| 2145 | Out = Atom. | |
| 2146 | annotate_undefined_ordering_definition_call(join(Arg1,Arg2,Type,POS), AnnotateWith, Annotated) :- | |
| 2147 | is_ordering_definition_call(Arg1), | |
| 2148 | !, | |
| 2149 | annotate_undefined_ordering_definition_call(Arg2, AnnotateWith, NArg2), | |
| 2150 | Annotated = join(Arg1,NArg2,Type,POS). | |
| 2151 | annotate_undefined_ordering_definition_call(join(Arg1,Arg2,Type,POS), AnnotateWith, Annotated) :- | |
| 2152 | is_ordering_definition_call(Arg2), | |
| 2153 | !, | |
| 2154 | annotate_undefined_ordering_definition_call(Arg1, AnnotateWith, NArg1), | |
| 2155 | Annotated = join(NArg1,Arg2,Type,POS). | |
| 2156 | annotate_undefined_ordering_definition_call(Binary, AnnotateWith, Annotated) :- | |
| 2157 | % TODO: nested join with different top-level ordering definition call here? | |
| 2158 | functor(Binary, BFun, 4), | |
| 2159 | !, | |
| 2160 | arg(1, Binary, Arg1), | |
| 2161 | arg(2, Binary, Arg2), | |
| 2162 | arg(3, Binary, Type), | |
| 2163 | arg(4, Binary, POS), | |
| 2164 | ( is_ordering_definition_call(Arg1) | |
| 2165 | -> get_alloy_position(Arg1, A1POS), | |
| 2166 | get_alloy_type(Arg1, Arg1Type), | |
| 2167 | NArg1 = join(AnnotateWith,Arg1,Arg1Type,A1POS) | |
| 2168 | ; annotate_undefined_ordering_definition_call(Arg1, AnnotateWith, NArg1) | |
| 2169 | ), | |
| 2170 | ( is_ordering_definition_call(Arg2) | |
| 2171 | -> get_alloy_position(Arg2, A2POS), | |
| 2172 | get_alloy_type(Arg2, Arg2Type), | |
| 2173 | NArg2 = join(AnnotateWith,Arg2,Arg2Type,A2POS) | |
| 2174 | ; annotate_undefined_ordering_definition_call(Arg2, AnnotateWith, NArg2) | |
| 2175 | ), | |
| 2176 | functor(Annotated, BFun, 4), | |
| 2177 | arg(1, Annotated, NArg1), | |
| 2178 | arg(2, Annotated, NArg2), | |
| 2179 | arg(3, Annotated, Type), | |
| 2180 | arg(4, Annotated, POS). | |
| 2181 | annotate_undefined_ordering_definition_call(AlloyTerm, _, AlloyTerm). | |
| 2182 | ||
| 2183 | atom_ends_with(Atom, EndsWith) :- | |
| 2184 | atom_concat(_, EndsWith, Atom). | |
| 2185 | ||
| 2186 | % ordering function calls like s.next.next are converted to fun_call | |
| 2187 | translate_join(_, Arg1, Arg2, TBinaryJoin) :- | |
| 2188 | Arg2 = fun_call(Name,[],Type,A2Pos), | |
| 2189 | \+ atom_prefix('integer', Name), | |
| 2190 | \+ atom_ends_with(Name, 'first'), % one can use just first or last without a join while the actual Signature is inferred by its type | |
| 2191 | \+ atom_ends_with(Name, 'last'), % e.g., see ring_election1.als 'no elected.first' where elected is an ordered signature field of sig P | |
| 2192 | % 'no elected.first' is thus equivalent to 'no elected.(P.first)' | |
| 2193 | translate_e_p(fun_call(Name,[Arg1],Type,A2Pos), TBinaryJoin). | |
| 2194 | % Translation of the dot join operator has several special cases depending on the arity of the arguments. | |
| 2195 | translate_join(TPos, Arg1, Arg2, TBinaryJoin) :- | |
| 2196 | translate_e_p(Arg1, TArg1), | |
| 2197 | translate_e_p(Arg2, TArg2), | |
| 2198 | translate_join_aux(TPos, Arg1, Arg2, TArg1, TArg2, TBinaryJoin). | |
| 2199 | ||
| 2200 | % Note: N-ary relation are encoded in B as follows: | |
| 2201 | % { (e1 |-> (e2 |-> (e3 |-> ...))) ,... }, for example: | |
| 2202 | % {(tracy|->(spanish|->french)),(carol|->(spanish|->french)), ...} | |
| 2203 | % univ.P --> ran(P) % this does NOT work for ternary,... relations | |
| 2204 | translate_join_aux(TPos, Arg1, Arg2, _TArg1, TArg2, range(TPos,TArg2)) :- | |
| 2205 | is_univ(Arg1), | |
| 2206 | is_binary_relation(Arg2), | |
| 2207 | !. | |
| 2208 | % P.univ --> dom(P) % this works for ternary,... relations | |
| 2209 | translate_join_aux(TPos, _Arg1, Arg2, TArg1, _TArg2, domain(TPos,TArg1)) :- | |
| 2210 | is_univ(Arg2), | |
| 2211 | !. | |
| 2212 | % {el}.R --> {R(el)} | |
| 2213 | translate_join_aux(TPos, Arg1, Arg2, TArg1, TArg2, set_extension(TPos,[function(TPos,TArg2,[TTArg1])])) :- | |
| 2214 | get_type_and_arity_from_alloy_term(Arg1, Type1, Arity), | |
| 2215 | Arity = 1, % is_unary_relation(Arg1), | |
| 2216 | is_binary_relation(Arg2), % TO DO: Arg2 can probably be n-ary? | |
| 2217 | is_total_function(TArg2, Type1), | |
| 2218 | can_remove_singleton_set(TArg1, TTArg1), | |
| 2219 | !. | |
| 2220 | % unary.R --> R[unary] | |
| 2221 | translate_join_aux(TPos, Arg1, Arg2, TArg1, TArg2, Join) :- % Unary.Arg2 --> Arg2[Unary] | |
| 2222 | is_unary_relation(Arg1), | |
| 2223 | is_binary_relation(Arg2), | |
| 2224 | !, | |
| 2225 | Join = image(TPos,TArg2,TArg1). | |
| 2226 | % binary.unary | |
| 2227 | % Next RULE is broken, can lead to Type errors and test is wrong: | |
| 2228 | % translate_join_aux(Pos,Arg1,Arg2,TArg1,TArg2,function(Pos,reverse(Pos,TArg1),[TTArg2])) :- | |
| 2229 | % % function call if lhs is a total function and rhs a unary relation | |
| 2230 | % is_binary_relation(Arg1), | |
| 2231 | % is_unary_relation(Arg2), | |
| 2232 | % is_total_function(TArg1) , ! , % TEST SHOULD BE SURJECTIVE and INJECTIVE !! | |
| 2233 | % remove_singleton_set(TArg2,TTArg2). | |
| 2234 | % Arg1.Unary --> Arg1~[Unary] | |
| 2235 | translate_join_aux(TPos, _Arg1, Arg2, TArg1, TArg2, image(TPos,reverse(TPos,TArg1),TArg2)) :- | |
| 2236 | is_unary_relation(Arg2), | |
| 2237 | !. | |
| 2238 | % binary.binary: Arg1.Arg2 --> (Arg1 ; Arg2) | |
| 2239 | translate_join_aux(TPos, Arg1, Arg2, TArg1, TArg2, composition(TPos,TArg1,TArg2)) :- | |
| 2240 | is_binary_relation(Arg1), | |
| 2241 | is_binary_relation(Arg2), | |
| 2242 | !. | |
| 2243 | translate_join_aux(TPos, Arg1, Arg2, TArg1, TArg2, comprehension_set(TPos,IDS,Body)) :- | |
| 2244 | Body = conjunct(TPos,TypingPred,exists(TPos,[JoinID],conjunct(TPos,JoinTypingPred,conjunct(TPos,Mem1,Mem2)))), | |
| 2245 | get_type_and_arity_from_alloy_term(Arg2, [JoinIDType|RTypes], Arity), % first type refers to outter variable | |
| 2246 | gen_ids_and_couple(Arity, IDs2, Couple2), | |
| 2247 | IDs2 = [JoinID|Rest2], | |
| 2248 | get_typing_pred_for_ids(TPos, RTypes, Rest2, TypingPred), | |
| 2249 | get_typing_pred_for_ids(TPos, [JoinIDType], [JoinID], JoinTypingPred), | |
| 2250 | ( is_univ(Arg1) -> | |
| 2251 | Mem1 = truth(TPos), | |
| 2252 | IDS = Rest2 | |
| 2253 | ; is_unary_relation(Arg1) -> | |
| 2254 | %strip_singleton_set_from_this(TArg1, TTArg1), | |
| 2255 | Mem1 = member(TPos,JoinID,TArg1), | |
| 2256 | IDS = Rest2 | |
| 2257 | ; gen_identifier(0, "_c_", ID0), | |
| 2258 | IDS = [ID0|Rest2], | |
| 2259 | Mem1 = member(TPos,couple(TPos,ID0,JoinID),TArg1) | |
| 2260 | ), | |
| 2261 | check_position(TPos,translate_join_aux), | |
| 2262 | Mem2 = member(TPos,Couple2,TArg2). | |
| 2263 | translate_join_aux(Pos, Arg1, Arg2, _TArg1, _TArg2, empty_set(Pos)) :- | |
| 2264 | format('~nJoin not supported this way:~nLeft: ~w~nRight: ~w~n', [Arg1,Arg2]), | |
| 2265 | add_error(load_alloy_model, 'Cannot translate this type of join yet', [Arg1,Arg2], Pos). | |
| 2266 | ||
| 2267 | % This predicate relies on the order of elements in 2. and 3. argument for typing. | |
| 2268 | % TO DO: improve | |
| 2269 | get_typing_pred_for_ids(Pos, [], [], truth(Pos)). | |
| 2270 | get_typing_pred_for_ids(Pos, [Type|TT], [ID|IT], TypingPred) :- | |
| 2271 | translate_e_p(Type, TType), | |
| 2272 | get_typing_pred_for_ids_acc(Pos, TT, IT, member(Pos,ID,TType), TypingPred). | |
| 2273 | ||
| 2274 | get_typing_pred_for_ids_acc(_, [], [], Acc, Acc). | |
| 2275 | get_typing_pred_for_ids_acc(Pos, [Type|TT], [ID|IT], Acc, TypingPred) :- | |
| 2276 | translate_e_p(Type, TType), | |
| 2277 | get_typing_pred_for_ids_acc(Pos, TT, IT, conjunct(Pos,Acc,member(Pos,ID,TType)), TypingPred). | |
| 2278 | ||
| 2279 | % translate Alloy position to B position | |
| 2280 | translate_pos(Var,Res) :- \+ ground(Var),!, | |
| 2281 | add_internal_error('Translating non-ground Alloy position to none:',translate_pos(Var,Res)), | |
| 2282 | Res=none. | |
| 2283 | translate_pos(pos(Col,Row), Res) :- nonvar(Col), nonvar(Row), | |
| 2284 | !, | |
| 2285 | row_col_to_position(Row,Col,Res). | |
| 2286 | translate_pos(_, none). | |
| 2287 | ||
| 2288 | %get_position(Term, BPos) :- | |
| 2289 | % get_alloy_position(Term, APos), | |
| 2290 | % !, | |
| 2291 | % translate_pos(APos, BPos). | |
| 2292 | %get_position(_, none). | |
| 2293 | ||
| 2294 | get_alloy_type(Term, AType) :- | |
| 2295 | functor(Term, _, Arity), | |
| 2296 | Arity > 0, | |
| 2297 | Arity1 is Arity - 1, | |
| 2298 | arg(Arity1, Term, AType). | |
| 2299 | ||
| 2300 | get_alloy_position(Term, APos) :- | |
| 2301 | functor(Term, _, Arity), | |
| 2302 | Arity > 0, | |
| 2303 | arg(Arity, Term, APos). | |
| 2304 | ||
| 2305 | get_b_position(UntypedBAst, BPOS) :- | |
| 2306 | functor(UntypedBAst, _, Arity), | |
| 2307 | Arity > 0, | |
| 2308 | arg(1, UntypedBAst, BPOS). | |
| 2309 | ||
| 2310 | check_position(Var,PP) :- var(Var),!,add_internal_error('Variable position at: ',PP),Var=none. | |
| 2311 | check_position(P,_) :- is_valid_position(P),!. | |
| 2312 | check_position(T,PP) :- add_warning(check_position,'Unknown position at: ',PP:T). | |
| 2313 | ||
| 2314 | translate_quantified_e(Pos, no, TArg, equal(Pos,TArg,empty_set(none))). | |
| 2315 | translate_quantified_e(Pos, AlloyKw, TArg, equal(Pos,card(none,TArg),integer(none,1))) :- | |
| 2316 | % naming possibly differs having the same semantics | |
| 2317 | AlloyKw = one; AlloyKw = oneof. | |
| 2318 | translate_quantified_e(Pos, AlloyKw, TArg, greater(Pos,card(none,TArg),integer(none,0))) :- | |
| 2319 | AlloyKw = some; AlloyKw = someof. | |
| 2320 | translate_quantified_e(Pos, AlloyKw, TArg, less_equal(Pos,card(none,TArg),integer(none,1))) :- | |
| 2321 | AlloyKw = lone; AlloyKw = loneof. | |
| 2322 | translate_quantified_e(_, exactlyof, TArg, TArg). | |
| 2323 | ||
| 2324 | % Join a list of types using cartesian_product like ((A*B)*C) for types [A,B,C]. | |
| 2325 | create_cartesian_type([ID], TID) :- | |
| 2326 | !, | |
| 2327 | translate_unary_e_p(ID, TID). | |
| 2328 | create_cartesian_type([ID1,ID2], cartesian_product(none,TID1,TID2)) :- | |
| 2329 | !, | |
| 2330 | translate_unary_e_p(ID1, TID1), | |
| 2331 | translate_unary_e_p(ID2, TID2). | |
| 2332 | create_cartesian_type([ID1,ID2|T], cartesian_product(none,cartesian_product(none,TID1,TID2),NT)) :- | |
| 2333 | translate_unary_e_p(ID1, TID1), | |
| 2334 | translate_unary_e_p(ID2, TID2), | |
| 2335 | create_cartesian_type(T, NT). | |
| 2336 | ||
| 2337 | % Field declarations have several special cases depending on the keywords set, one, some, lone or seq. | |
| 2338 | % We are inside Signature TSignatureName sig NAME { field : DeclTerm } | |
| 2339 | translate_field_decl(BPOS, SignatureName, TSignatureName, DeclTerm, FieldID, TFieldID, TFieldPred) :- | |
| 2340 | % DeclTerm =.. [_,SetID|_], | |
| 2341 | replace_this_in_signature_field(DeclTerm, NewDeclTerm), | |
| 2342 | debug_format(19, 'Translating Field ~w inside signature ~w,~n Term=~w,~n~n', [FieldID,SignatureName,NewDeclTerm]), | |
| 2343 | ( translate_special_field_multiplicity_binary_e_p(NewDeclTerm, TFUNC) | |
| 2344 | -> | |
| 2345 | % we could do: translate_cartesian2(BPOS,TSignatureName,NewDeclTerm,Cart), TFieldPred = subset(BPOS,TFieldID,Cart), and add predicate | |
| 2346 | % TO DO: better treatment, also detect nested special multiplicity annotations inside NewDeclTerm | |
| 2347 | % generate forall x:SIG => x.field : TFUNC | |
| 2348 | ID = identifier(BPOS,'_x_'), | |
| 2349 | AID = identifier('_x_',type([SignatureName],1),none), | |
| 2350 | ( singleton_set('_x_') -> | |
| 2351 | true | |
| 2352 | ; assert_singleton_set('_x_') | |
| 2353 | ), | |
| 2354 | translate_e_p(AID, TAID), % will add set-extension wrapper | |
| 2355 | LHS = member(BPOS,ID,TSignatureName), | |
| 2356 | RHS = member(BPOS,TJoin,TFUNC), | |
| 2357 | TFieldPred = conjunct(BPOS,FieldTyping,forall(BPOS,[ID],implication(none,LHS,RHS))), | |
| 2358 | translate_join_aux(BPOS, AID, FieldID, TAID, TFieldID, TJoin), | |
| 2359 | get_type_and_arity_from_alloy_term(FieldID, TypeList, _), | |
| 2360 | create_cartesian_type(TypeList, CartesianType), | |
| 2361 | FieldTyping = member(BPOS,TFieldID,pow_subset(BPOS,CartesianType)) | |
| 2362 | ; translate_sig_field_rhs(FieldID, NewDeclTerm, BPOS, TSignatureName, TFieldID, FieldTypeExpr) | |
| 2363 | -> | |
| 2364 | add_constraint_for_someof_field(NewDeclTerm, member(BPOS,TFieldID,FieldTypeExpr), TSignatureName, TTFieldPred), | |
| 2365 | add_constraint_for_seq_field(NewDeclTerm, TSignatureName, TTFieldPred, TFieldID, TFieldPred) | |
| 2366 | ; add_error(alloy2b, 'Field declaration not implemented:', NewDeclTerm, BPOS), | |
| 2367 | TFieldPred = truth(none) | |
| 2368 | ). | |
| 2369 | ||
| 2370 | add_constraint_for_someof_field(someof(_,_,_), TempPred, TSignatureName, TPred) :- | |
| 2371 | !, | |
| 2372 | TempPred = member(BPOS,TFieldID,_), | |
| 2373 | TPred = conjunct(BPOS,equal(BPOS,domain(BPOS,TFieldID),TSignatureName),TempPred). | |
| 2374 | add_constraint_for_someof_field(_, Pred, _, Pred). | |
| 2375 | ||
| 2376 | add_constraint_for_seq_field('is_seq'(_,_,_), TSignatureName, TempPred, TFieldID, TPred) :- | |
| 2377 | !, | |
| 2378 | % !_s.(_s : TSignatureName => dom(TFieldID)[{_s}] = 0..card(dom(TFieldID)[{_s}])-1) | |
| 2379 | TPred = conjunct(BPOS,TempPred,forall([identifier(BPOS,'_s')], | |
| 2380 | implication(BPOS,member(identifier(BPOS,'_s'),TSignatureName), | |
| 2381 | equal(BPOS,image(BPOS,domain(BPOS,TFieldID),set_extension(BPOS,[identifier(BPOS,'_s')])), | |
| 2382 | interval(BPOS,integer(BPOS,0),minus(BPOS,card(BPOS,image(BPOS,domain(BPOS,TFieldID), | |
| 2383 | set_extension(BPOS,[identifier(BPOS,'_s')]))),integer(BPOS,1))))))). | |
| 2384 | add_constraint_for_seq_field(_, _, Pred, _, Pred). | |
| 2385 | ||
| 2386 | % sig SIG { field : set Set} --> field : SIG <-> Set | |
| 2387 | translate_sig_field_rhs(_, setof(Set,_,_), _, SIG, _, relations(none,SIG,TSet)) :- | |
| 2388 | translate_e_p(Set, TSet). | |
| 2389 | % sig SIG { field : one Set} --> field : SIG --> Set | |
| 2390 | translate_sig_field_rhs(_, oneof(Set,_,_), _, SIG, TFieldID, total_function(none,SIG,TSet)) :- | |
| 2391 | translate_e_p(Set, TSet), | |
| 2392 | assert_total_function(TFieldID, SIG). | |
| 2393 | % sig SIG { field : lone Set} --> field : SIG +-> Set | |
| 2394 | translate_sig_field_rhs(_, loneof(Set,_,_), _, SIG, _, partial_function(none,SIG,TSet)) :- | |
| 2395 | translate_e_p(Set, TSet). | |
| 2396 | % sig SIG { field : some Set} --> field : SIG +-> Set | |
| 2397 | translate_sig_field_rhs(_, someof(Set,_,_), _, SIG, _, relations(none,SIG,TSet)) :- | |
| 2398 | translate_e_p(Set, TSet). | |
| 2399 | % sig SIG { field : seq Set} --> field : (SIG * Integer) +-> Set | |
| 2400 | translate_sig_field_rhs(FieldID, 'is_seq'(_,Set,_,_), _, SIG, _, partial_function(none,cartesian_product(none,SIG,interval(none,integer(none,0),integer(none,MaxSeq1))),TSet)) :- | |
| 2401 | maxseq(MaxSeq), | |
| 2402 | MaxSeq1 is MaxSeq - 1, | |
| 2403 | FieldID = identifier(Name,Type,_), | |
| 2404 | prepend_identifier_of_module_import(Name, Type, NName), | |
| 2405 | assertz(is_seq(NName)), | |
| 2406 | translate_e_p(Set, TSet). | |
| 2407 | % sig SIG { field : FieldTerm} --> field : POW(SIG * FieldTerm) | |
| 2408 | translate_sig_field_rhs(_, FieldTerm, Pos, SIG, _, pow_subset(none,Cart)) :- | |
| 2409 | % TO DO: check whether lone, one, ... can appear inside FieldTerm | |
| 2410 | translate_cartesian2(Pos, SIG, FieldTerm, Cart). | |
| 2411 | ||
| 2412 | replace_this_in_signature_field(identifier('this',type([SignatureName],1),Pos), Res) :- | |
| 2413 | !, | |
| 2414 | Res = identifier(SignatureName,type([SignatureName],1),Pos). | |
| 2415 | replace_this_in_signature_field(DeclTerm, NewDeclTerm) :- | |
| 2416 | DeclTerm =.. [Functor,Arg1,Type,Pos], | |
| 2417 | !, | |
| 2418 | replace_this_in_signature_field(Arg1, NArg1), | |
| 2419 | NewDeclTerm =.. [Functor,NArg1,Type,Pos]. | |
| 2420 | replace_this_in_signature_field(DeclTerm, NewDeclTerm) :- | |
| 2421 | DeclTerm =.. [Functor,Arg1,Arg2,Type,Pos], | |
| 2422 | !, | |
| 2423 | replace_this_in_signature_field(Arg1, NArg1), | |
| 2424 | replace_this_in_signature_field(Arg2, NArg2), | |
| 2425 | NewDeclTerm =.. [Functor,NArg1,NArg2,Type,Pos]. | |
| 2426 | replace_this_in_signature_field(DeclTerm, DeclTerm). | |
| 2427 | ||
| 2428 | % Translate TFieldID: Declaration | |
| 2429 | fun_or_pred_decl_special_cases(setof(Expr,_,_), TFieldID, Pos, subset(Pos,TFieldID,TExpr), set) :- | |
| 2430 | translate_e_p(Expr, TExpr). | |
| 2431 | fun_or_pred_decl_special_cases(oneof(Expr,_,_), TFieldID, Pos, subset(Pos,TFieldID,TExpr), singleton) :- % Default | |
| 2432 | translate_e_p(Expr, TExpr). | |
| 2433 | fun_or_pred_decl_special_cases(loneof(Expr,_,_), TFieldID, Pos, conjunct(Pos,subset(Pos,TFieldID,TExpr),ExtraPred), set) :- | |
| 2434 | % x : lone S -> x <: S & card(x) <= 1 | |
| 2435 | ExtraPred = less_equal(Pos,card(Pos,TFieldID),integer(Pos,1)), | |
| 2436 | translate_e_p(Expr, TExpr). | |
| 2437 | fun_or_pred_decl_special_cases(someof(Expr,_,_), TFieldID, Pos, conjunct(Pos,subset(Pos,TFieldID,TExpr),ExtraPred), set) :- | |
| 2438 | % x : some S -> x <: S & x \= {} | |
| 2439 | ExtraPred = not_equal(Pos,TFieldID,empty_set(Pos)), | |
| 2440 | translate_e_p(Expr, TExpr). | |
| 2441 | fun_or_pred_decl_special_cases(Expr, TFieldID, Pos, Translation, IsSingleton) :- | |
| 2442 | % treat identifier, cartesian, union, ... use translate of TFieldID in Expr | |
| 2443 | translate_binary_in(TFieldID, Expr, Pos, Translation), | |
| 2444 | get_type_and_arity_from_alloy_term(Expr, _Type, Arity), | |
| 2445 | !, | |
| 2446 | ( Arity = 1 -> | |
| 2447 | IsSingleton = singleton | |
| 2448 | ; IsSingleton = set | |
| 2449 | ). | |
| 2450 | fun_or_pred_decl_special_cases(Term, _, Pos, falsity(Pos), set) :- | |
| 2451 | add_error(alloy2b, 'Field declaration for function or predicate not implemented:', Term, Pos). | |
| 2452 | ||
| 2453 | alloy_to_b_operator(Op, BOp) :- | |
| 2454 | alloy_to_b_unary_operator(Op, BOp), | |
| 2455 | !. | |
| 2456 | alloy_to_b_operator(Op, BOp) :- | |
| 2457 | alloy_to_b_binary_operator(Op, BOp), | |
| 2458 | !. | |
| 2459 | alloy_to_b_operator(Op, Op) :- | |
| 2460 | format('~n~nTRANSLATING ~w to B without modification!~n', [Op]). | |
| 2461 | ||
| 2462 | alloy_to_b_unary_operator(not, negation). | |
| 2463 | alloy_to_b_unary_operator(closure1, closure). | |
| 2464 | alloy_to_b_unary_operator(closure, reflexive_closure). | |
| 2465 | alloy_to_b_unary_operator(inverse, reverse). % works for binary relation only; indeed Alloy says: ~ can be used only with a binary relation. | |
| 2466 | ||
| 2467 | ||
| 2468 | alloy_to_b_binary_operator(in, subset). | |
| 2469 | alloy_to_b_binary_operator(not_in, not_subset). | |
| 2470 | alloy_to_b_binary_operator(plus, union). | |
| 2471 | alloy_to_b_binary_operator(or, disjunct). % actually treated as unary operator | |
| 2472 | alloy_to_b_binary_operator(and, conjunct). % actually treated as unary operator | |
| 2473 | alloy_to_b_binary_operator(minus, set_subtraction). | |
| 2474 | % alloy_to_b_binary_operator(cartesian,cartesian_product). % only works for X->UNARY ! | |
| 2475 | alloy_to_b_binary_operator(function, expression_definition). | |
| 2476 | alloy_to_b_binary_operator(predicate, predicate_definition). | |
| 2477 | alloy_to_b_binary_operator(not_equal, not_equal). | |
| 2478 | alloy_to_b_binary_operator(dom_restr, domain_restriction). % not ok for ternary, set must be unary | |
| 2479 | alloy_to_b_binary_operator(ran_restr, range_restriction). % also ok for ternary, ... relations | |
| 2480 | alloy_to_b_binary_operator(equal, equal). | |
| 2481 | alloy_to_b_binary_operator(conjunct, conjunct). | |
| 2482 | alloy_to_b_binary_operator(intersection, intersection). | |
| 2483 | alloy_to_b_binary_operator(implication, implication). | |
| 2484 | alloy_to_b_binary_operator(iff, equivalence). | |
| 2485 | alloy_to_b_binary_operator(override, overwrite). % ++ | |
| 2486 | ||
| 2487 | is_cartesian_product_term(Term, Arg1, Arg2, POS) :- | |
| 2488 | functor(Term, Functor, 4), | |
| 2489 | is_cartesian_product(Functor), | |
| 2490 | arg(1, Term, Arg1), | |
| 2491 | arg(2, Term, Arg2), | |
| 2492 | arg(4, Term, POS). | |
| 2493 | is_cartesian_product(cartesian). | |
| 2494 | ||
| 2495 | ||
| 2496 | % predicates with integer arguments | |
| 2497 | alloy_to_b_integer_operator(less, less). | |
| 2498 | alloy_to_b_integer_operator(greater, greater). | |
| 2499 | alloy_to_b_integer_operator(less_equal, less_equal). | |
| 2500 | alloy_to_b_integer_operator(greater_equal, greater_equal). | |
| 2501 | ||
| 2502 | ||
| 2503 | %%% | |
| 2504 | % Accumulate the translated machine parts and signature names during the translation and build the machine AST afterwards. | |
| 2505 | % We may need the signature names later on if translating a global scope. | |
| 2506 | build_machine_ast(b_machine(ListOfMachineParts,_SignatureNames), machine(generated(none,AbstractMachine))) :- | |
| 2507 | % filter empty machine parts | |
| 2508 | findall(MachinePart, ( member(MachinePart, ListOfMachineParts), | |
| 2509 | arg(2,MachinePart,L), | |
| 2510 | L \== [] | |
| 2511 | ), NonEmptyMachineSections), | |
| 2512 | % properties need to be conjoined | |
| 2513 | ( select(properties(none,L), NonEmptyMachineSections, RestListOfUsedMachineParts) -> | |
| 2514 | true | |
| 2515 | ; L == [], | |
| 2516 | RestListOfUsedMachineParts = NonEmptyMachineSections | |
| 2517 | ), | |
| 2518 | join_predicates(conjunct, L, FlatL), | |
| 2519 | AbstractMachine = abstract_machine(none,machine(none), | |
| 2520 | machine_header(none,alloytranslation,[]), | |
| 2521 | [properties(none,FlatL)|RestListOfUsedMachineParts]), | |
| 2522 | !. | |
| 2523 | ||
| 2524 | empty_machine_acc(b_machine([sets(none,[]),constants(none,[]), | |
| 2525 | definitions(none,[]),properties(none,[]), | |
| 2526 | assertions(none,[]),operations(none,[])],[])). | |
| 2527 | ||
| 2528 | % extend a machine section with a give list of conjuncts | |
| 2529 | extend_machine_with_conjuncts(_Section, [], Acc, Res) :- | |
| 2530 | !, | |
| 2531 | Res = Acc. | |
| 2532 | extend_machine_with_conjuncts(Section, Conjuncts, MAcc1, MAcc2) :- | |
| 2533 | join_untyped_ast_nodes(conjunct, Conjuncts, TPred), | |
| 2534 | extend_machine_acc(Section, MAcc1, TPred, MAcc2). | |
| 2535 | ||
| 2536 | :- if(environ(prob_safe_mode,true)). | |
| 2537 | extend_machine_acc(F, _, New, _) :- \+ ground(New), | |
| 2538 | add_internal_error('Non-ground new formula:',extend_machine_acc(F, _, New, _)), | |
| 2539 | fail. | |
| 2540 | :- endif. | |
| 2541 | extend_machine_acc(signatures, b_machine(MachineParts,SignatureNames), New, | |
| 2542 | b_machine(MachineParts,NewSignatureNames)) :- | |
| 2543 | !, | |
| 2544 | append(SignatureNames, New, TSignatureNames), | |
| 2545 | remove_dups(TSignatureNames, NewSignatureNames). | |
| 2546 | extend_machine_acc(Functor, b_machine(MachineParts,SignatureNames), New, | |
| 2547 | b_machine([NewMachinePart|RestMachineParts],SignatureNames)) :- | |
| 2548 | MachinePart =.. [Functor,none,List], | |
| 2549 | select(MachinePart, MachineParts, RestMachineParts), | |
| 2550 | append(List, [New], NewList), % keeps order, but is inefficient! | |
| 2551 | NewMachinePart =.. [Functor,none,NewList], | |
| 2552 | !. | |
| 2553 | extend_machine_acc(Functor, _, _, _) :- | |
| 2554 | add_internal_error('Failed: ', extend_machine_acc(Functor,_,_,_)), | |
| 2555 | fail. | |
| 2556 | ||
| 2557 | get_signature_names_from_machine_acc(b_machine(_MachineParts,SignatureNames), SignatureNames). | |
| 2558 | ||
| 2559 | finalize_extending_signatures(MAcc, NewMAcc) :- | |
| 2560 | extending_signatures(List), | |
| 2561 | !, | |
| 2562 | finalize_extending_signatures_aux(MAcc, List, NewMAcc). | |
| 2563 | finalize_extending_signatures(MAcc, MAcc). | |
| 2564 | ||
| 2565 | finalize_extending_signatures_aux(MAcc, [], MAcc). | |
| 2566 | finalize_extending_signatures_aux(MAcc, [(Parent,SubSigs)|T], NewMAcc) :- | |
| 2567 | length(SubSigs, AmountOfSubSigs), | |
| 2568 | AmountOfSubSigs > 1, | |
| 2569 | !, | |
| 2570 | maplist(translate_sub_sig, SubSigs, TSubSigs), | |
| 2571 | translate_e_p(Parent, TParent), | |
| 2572 | extend_machine_acc(properties, MAcc, partition(none,TParent,TSubSigs), MAcc2), | |
| 2573 | % equivalent to | |
| 2574 | % parent = sub1 \/ sub2 \/ ... \/ subN & sub1 /\ sub2 = {} & ... | |
| 2575 | findall(OneSub, member(OneSub/one, SubSigs), OneSubSigs), | |
| 2576 | length(OneSubSigs, AmountOneSubSigs), | |
| 2577 | ( AmountOneSubSigs = AmountOfSubSigs % we basically have an enumerated set with only singleton elements | |
| 2578 | -> | |
| 2579 | extend_machine_acc(properties, MAcc2, equal(none,card(none,TParent),integer(none,AmountOneSubSigs)), MAcc3) | |
| 2580 | ; extend_machine_acc(properties, MAcc2, greater_equal(none,card(none,TParent),integer(none,AmountOneSubSigs)), MAcc3) | |
| 2581 | ), | |
| 2582 | finalize_extending_signatures_aux(MAcc3, T, NewMAcc). | |
| 2583 | finalize_extending_signatures_aux(MAcc, [_|T], NewMAcc) :- | |
| 2584 | finalize_extending_signatures_aux(MAcc, T, NewMAcc). | |
| 2585 | %%% | |
| 2586 | translate_sub_sig(Name/_One, B) :- | |
| 2587 | translate_e_p(Name, B). | |
| 2588 | ||
| 2589 | assert_extending_signature(Name, Parent, One) :- | |
| 2590 | ( is_sub_signature_of(Name, Parent, One) -> | |
| 2591 | true | |
| 2592 | ; debug_format(19, '~w is sub signature of ~w (~w)~n', [Name,Parent,One]), | |
| 2593 | assertz(is_sub_signature_of(Name, Parent, One)) | |
| 2594 | ), | |
| 2595 | extending_signatures(List), | |
| 2596 | select((Parent,SubSigs), List, Rest), | |
| 2597 | !, | |
| 2598 | ( \+ memberchk(Name/One, SubSigs) | |
| 2599 | -> | |
| 2600 | retractall(extending_signatures(_)), | |
| 2601 | asserta(extending_signatures([(Parent,[Name/One|SubSigs])|Rest])) | |
| 2602 | ; true | |
| 2603 | ). | |
| 2604 | assert_extending_signature(Name, Parent, One) :- | |
| 2605 | retract(extending_signatures(List)), | |
| 2606 | !, | |
| 2607 | asserta(extending_signatures([(Parent,[Name/One])|List])). | |
| 2608 | assert_extending_signature(Name, Parent, One) :- | |
| 2609 | asserta(extending_signatures([(Parent,[Name/One])])). | |
| 2610 | ||
| 2611 | assert_enumerated_set(Options, Name) :- | |
| 2612 | % singleton top-level signatures are defined as an enumerated set like S = {_S} | |
| 2613 | member(one, Options), | |
| 2614 | % but extending singleton signatures are defined as constants and singleton subsets of their parent type | |
| 2615 | \+ member(subset(_), Options), | |
| 2616 | \+ member(subsig(_), Options), | |
| 2617 | !, | |
| 2618 | asserta(enumerated_set(Name)). | |
| 2619 | assert_enumerated_set(_, _). | |
| 2620 | ||
| 2621 | assert_abstract_sig(Options, Name) :- | |
| 2622 | member(abstract, Options), | |
| 2623 | !, | |
| 2624 | asserta(abstract_sig(Name)). | |
| 2625 | assert_abstract_sig(_, _). | |
| 2626 | ||
| 2627 | assert_singleton_set(Options, Name) :- | |
| 2628 | member(one, Options), | |
| 2629 | !, | |
| 2630 | assert_singleton_set(Name). | |
| 2631 | assert_singleton_set(_, _). | |
| 2632 | ||
| 2633 | assert_singleton_set(Name) :- % debug_format(19,'Singleton set : ~w~n',[Name]),nl, | |
| 2634 | % \+ singleton_set(Name), | |
| 2635 | asserta(singleton_set(Name)), | |
| 2636 | !. | |
| 2637 | % assert_singleton_set(_). | |
| 2638 | retract_singleton_set(BPOS, Name) :- | |
| 2639 | ( retract(singleton_set(Name)) -> | |
| 2640 | true | |
| 2641 | ; | |
| 2642 | add_message(retract_singleton_set, 'WARNING: no singleton_set fact for: ', Name, BPOS) % can be ok for non-singleton ids | |
| 2643 | ). | |
| 2644 | % retractall(singleton_set(Name)). | |
| 2645 | retract_state :- | |
| 2646 | % don't retract model_path here | |
| 2647 | retractall(fact(_)), | |
| 2648 | retractall(assertion(_)), | |
| 2649 | retractall(definition_without_param(_)), | |
| 2650 | retractall(skipped_command(_,_)), | |
| 2651 | retractall(translated_command(_,_)), | |
| 2652 | retractall(abstract_sig(_)), | |
| 2653 | retractall(sig_field_id(_, _)), | |
| 2654 | retractall(artificial_parent_type(_, _, _)), | |
| 2655 | retractall(current_module_in_scope(_)), | |
| 2656 | retractall(module_in_scope_but_root(_, _)), | |
| 2657 | retractall(enumerated_set(_)), | |
| 2658 | retractall(singleton_set(_)), | |
| 2659 | retractall(ordered_signature(_)), | |
| 2660 | retractall(total_function(_, _)), | |
| 2661 | retractall(extending_signatures(_)), | |
| 2662 | retractall(is_seq(_)), | |
| 2663 | retractall(maxseq(_)), | |
| 2664 | retractall(is_sub_signature_of(_, _, _)), | |
| 2665 | !. | |
| 2666 | ||
| 2667 | % an identifier which in B refers not to a set but an element of a set, representing a singleton set in Alloy | |
| 2668 | is_singleton_set_id(this). % this is always singleton (TO DO: check this ;-) | |
| 2669 | is_singleton_set_id(IDName) :- | |
| 2670 | singleton_set(IDName). | |
| 2671 | ||
| 2672 | assert_total_function(identifier(_,Name), SIG) :- | |
| 2673 | !, | |
| 2674 | assert_total_function(Name, SIG). | |
| 2675 | assert_total_function(Name, identifier(_,SIG)) :- | |
| 2676 | !, | |
| 2677 | assert_total_function(Name, SIG). | |
| 2678 | assert_total_function(Name, SIG) :- | |
| 2679 | debug_format(19, 'Total function ~w over ~w~n', [Name,SIG]), | |
| 2680 | asserta(total_function(Name, SIG)). | |
| 2681 | ||
| 2682 | is_total_function(predecessor(_), _). % translation of prev | |
| 2683 | is_total_function(successor(_), _). % translation of next | |
| 2684 | is_total_function(function(_,ID,_), ArgType) :- | |
| 2685 | !, | |
| 2686 | is_total_function(ID, ArgType). | |
| 2687 | is_total_function(identifier(_,Name), ArgType) :- | |
| 2688 | !, | |
| 2689 | is_total_function(Name, ArgType). | |
| 2690 | is_total_function(Name, [ArgType]) :- | |
| 2691 | total_function(Name, FunType), % TO DO: check if FunctionType is Superset of ArgType | |
| 2692 | ( strip_singleton_set(FunType, SFunType), | |
| 2693 | SFunType = identifier(_,ArgType) | |
| 2694 | -> true | |
| 2695 | ; ArgType = FunType -> true | |
| 2696 | ; is_sub_signature_of(ArgType, FunType, _) | |
| 2697 | ). | |
| 2698 | ||
| 2699 | assert_ordered_sig_name(Name) :- | |
| 2700 | asserta(ordered_signature(Name)). | |
| 2701 | ||
| 2702 | is_ordered_signature(IDName) :- | |
| 2703 | ordered_signature(IDName). | |
| 2704 | is_ordered_signature('ordering\''). | |
| 2705 | ||
| 2706 | is_univ(identifier('univ',_,_)). % universe | |
| 2707 | is_univ(identifier(_,'univ')). | |
| 2708 | ||
| 2709 | is_iden(iden(_)). | |
| 2710 | is_iden(event_b_identity(_)). | |
| 2711 | ||
| 2712 | is_unary_relation(AlloyTerm) :- | |
| 2713 | get_type_and_arity_from_alloy_term(AlloyTerm, _Type, Arity), | |
| 2714 | Arity == 1. | |
| 2715 | ||
| 2716 | is_binary_relation(AlloyTerm) :- | |
| 2717 | get_type_and_arity_from_alloy_term(AlloyTerm, _Type, Arity), | |
| 2718 | Arity == 2. | |
| 2719 | ||
| 2720 | can_remove_singleton_set(set_extension(_,[Element]), Element). | |
| 2721 | % remove_singleton_set(AST,AST). | |
| 2722 | get_type_and_arity_from_alloy_term(integer(_,_), Type, Arity) :- | |
| 2723 | !, | |
| 2724 | Type = integer, | |
| 2725 | Arity = 1. % will get translated to singleton set | |
| 2726 | get_type_and_arity_from_alloy_term(and(_,_), Type, Arity) :- | |
| 2727 | !, | |
| 2728 | Type = [untyped], | |
| 2729 | Arity = 0. % predicate | |
| 2730 | get_type_and_arity_from_alloy_term(or(_,_), Type, Arity) :- | |
| 2731 | !, | |
| 2732 | Type = [untyped], | |
| 2733 | Arity = 0. % predicate | |
| 2734 | get_type_and_arity_from_alloy_term(iden(_), Type, Arity) :- | |
| 2735 | !, | |
| 2736 | Type = univ, | |
| 2737 | Arity = 2. | |
| 2738 | get_type_and_arity_from_alloy_term(AlloyTerm, Type, NArity) :- | |
| 2739 | AlloyTerm =.. [_|Args], | |
| 2740 | member(type(Type,Arity), Args), | |
| 2741 | ( is_primitive_type(Type, NArity) | |
| 2742 | ; | |
| 2743 | ( length(Type, LType), | |
| 2744 | LType == Arity, | |
| 2745 | NArity = Arity | |
| 2746 | ) | |
| 2747 | ), | |
| 2748 | !. | |
| 2749 | get_type_and_arity_from_alloy_term(AlloyTerm, Type, Arity) :- | |
| 2750 | add_warning(alloy2b, 'Could not extract type and arity from Alloy term:', AlloyTerm), | |
| 2751 | Type = [untyped], | |
| 2752 | Arity = 0. % like predicate | |
| 2753 | ||
| 2754 | % TO DO: maybe there are more primitive types? | |
| 2755 | % primitive types have arity zero in Alloy for some reason | |
| 2756 | is_primitive_type(['PrimitiveBoolean'], 1). | |
| 2757 | ||
| 2758 | % atom_or_identifier_term(ID,ID) :- atom(ID). | |
| 2759 | % atom_or_identifier_term(identifier(IDName,_,_),IDName). | |
| 2760 | join_predicates(Op, TArgList, TBinaryP) :- | |
| 2761 | alloy_to_b_operator(Op, BOp), | |
| 2762 | ( BOp = conjunct | |
| 2763 | ; BOp = disjunct | |
| 2764 | ), | |
| 2765 | join_untyped_ast_nodes(BOp, TArgList, TBinaryP). | |
| 2766 | ||
| 2767 | join_untyped_ast_nodes(_, [], truth(none)). | |
| 2768 | join_untyped_ast_nodes(BOp, [H|T], Conjoined) :- | |
| 2769 | join_untyped_ast_nodes(BOp, T, H, Conjoined). | |
| 2770 | ||
| 2771 | join_untyped_ast_nodes(_, [], Acc, Acc). | |
| 2772 | join_untyped_ast_nodes(BOp, [H|T], Acc, Conjoined) :- | |
| 2773 | NewAcc =.. [BOp,none,Acc,H], | |
| 2774 | join_untyped_ast_nodes(BOp, T, NewAcc, Conjoined). | |
| 2775 | ||
| 2776 | ||
| 2777 | %:- load_files(library(system), [when(compile_time), imports([environ/2])]). | |
| 2778 | :- if(environ(prob_release,true)). | |
| 2779 | % Don't include tests in release mode. | |
| 2780 | :- else. | |
| 2781 | ||
| 2782 | :- use_module(library(plunit)). | |
| 2783 | :- use_module(testsrc(test_paths), []). % set up prob_examples(...) alias | |
| 2784 | ||
| 2785 | :- begin_tests(full_machine_translation). | |
| 2786 | ||
| 2787 | test(cards, []) :- | |
| 2788 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/cards.pl')). | |
| 2789 | ||
| 2790 | test(filesystem, []) :- | |
| 2791 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/filesystem.pl')). | |
| 2792 | ||
| 2793 | test(filesystem2, []) :- | |
| 2794 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/filesystem2.pl')). | |
| 2795 | ||
| 2796 | test(self_grandpas, []) :- | |
| 2797 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/selfgrandpas.pl')). | |
| 2798 | ||
| 2799 | test(queens, []) :- | |
| 2800 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/queens.pl')). | |
| 2801 | ||
| 2802 | test(queens2, []) :- | |
| 2803 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/queens2.pl')). | |
| 2804 | ||
| 2805 | test(queens3, []) :- | |
| 2806 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/queens3.pl')). | |
| 2807 | ||
| 2808 | test(queens4, []) :- | |
| 2809 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/queens4.pl')). | |
| 2810 | ||
| 2811 | test(river_crossing, []) :- | |
| 2812 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/rivercrossingpuzzle.pl')). | |
| 2813 | ||
| 2814 | test(river_crossing_v2, []) :- | |
| 2815 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/rivercrossingpuzzle_v2.pl')). | |
| 2816 | ||
| 2817 | test(enum_test, []) :- | |
| 2818 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/enumtest.pl')). | |
| 2819 | ||
| 2820 | test(disj_field_test, []) :- | |
| 2821 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/disjfieldtest.pl')). | |
| 2822 | ||
| 2823 | test(crewAlloc, []) :- | |
| 2824 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/crewalloc.pl')). | |
| 2825 | ||
| 2826 | test(http, []) :- | |
| 2827 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/http.pl')). | |
| 2828 | ||
| 2829 | test(knights, []) :- | |
| 2830 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/knights_and_knaves.pl')). | |
| 2831 | ||
| 2832 | test(join_binary, []) :- | |
| 2833 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/joinbinary.pl')). | |
| 2834 | ||
| 2835 | test(slot_data_v2, []) :- | |
| 2836 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/slot_data_v2.pl')). | |
| 2837 | ||
| 2838 | test(job_puzzle, []) :- | |
| 2839 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/job_puzzle.pl')). | |
| 2840 | ||
| 2841 | test(natural, []) :- | |
| 2842 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/natural.pl')). | |
| 2843 | ||
| 2844 | test(mutex,[]) :- | |
| 2845 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/mutex.pl')). | |
| 2846 | ||
| 2847 | test(family_v1,[]) :- | |
| 2848 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/family-v1.pl')). | |
| 2849 | ||
| 2850 | test(unary_ordering_rewriting, []) :- | |
| 2851 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/unary_ordering_rewriting.pl')). | |
| 2852 | ||
| 2853 | test(einstein1, []) :- | |
| 2854 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/einstein1.pl')). | |
| 2855 | ||
| 2856 | test(einstein2, []) :- | |
| 2857 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/einstein2.pl')). | |
| 2858 | ||
| 2859 | test(einstein3, []) :- | |
| 2860 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/einstein3.pl')). | |
| 2861 | ||
| 2862 | test(einsteins_enum, []) :- | |
| 2863 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/einsteins_enum.pl')). | |
| 2864 | ||
| 2865 | test(nodeweightedgraph, []) :- | |
| 2866 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/nodeweightedgraph.pl')). | |
| 2867 | ||
| 2868 | test(lists, []) :- | |
| 2869 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/lists.pl')). | |
| 2870 | ||
| 2871 | test(peano, []) :- | |
| 2872 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/peano.pl')). | |
| 2873 | ||
| 2874 | test(random_games, []) :- | |
| 2875 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/random_games.pl')). | |
| 2876 | ||
| 2877 | test(ordering_test, []) :- | |
| 2878 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/ordering_test.pl')). | |
| 2879 | ||
| 2880 | test(rellaws, []) :- | |
| 2881 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/rellaws.pl')). | |
| 2882 | ||
| 2883 | test(color_australia, []) :- | |
| 2884 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/color_australia.pl')). | |
| 2885 | ||
| 2886 | test(add_addr_correct, []) :- | |
| 2887 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/add_addr_correct.pl')). | |
| 2888 | ||
| 2889 | test(ambiguous_field_name, []) :- | |
| 2890 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/ambiguous_field_name.pl')). | |
| 2891 | ||
| 2892 | test(ambiguous_quantifier_field_name, []) :- | |
| 2893 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/ambiguous_quantifier_field_name.pl')). | |
| 2894 | ||
| 2895 | test(arithmetic, []) :- | |
| 2896 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/arithmetic.pl')). | |
| 2897 | ||
| 2898 | test(card, []) :- | |
| 2899 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/card.pl')). | |
| 2900 | ||
| 2901 | test(binary_differently_typed, []) :- | |
| 2902 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/binary_differently_typed.pl')). | |
| 2903 | ||
| 2904 | test(extendedfilesystem, []) :- | |
| 2905 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/extendedfilesystem.pl')). | |
| 2906 | ||
| 2907 | test(generated200, []) :- | |
| 2908 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/generated200.pl')). | |
| 2909 | ||
| 2910 | test(generated400, []) :- | |
| 2911 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/generated400.pl')). | |
| 2912 | ||
| 2913 | test(proofexample, []) :- | |
| 2914 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/proofexample.pl')). | |
| 2915 | ||
| 2916 | test(quantifiers, []) :- | |
| 2917 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/quantifiers.pl')). | |
| 2918 | ||
| 2919 | test(multiplicities, []) :- | |
| 2920 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/multiplicities.pl')). | |
| 2921 | ||
| 2922 | test(joinbinarycomplex, []) :- | |
| 2923 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/joinbinarycomplex.pl')). | |
| 2924 | ||
| 2925 | test(relations, []) :- | |
| 2926 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/relations.pl')). | |
| 2927 | ||
| 2928 | test(restrictions, []) :- | |
| 2929 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/restrictions.pl')). | |
| 2930 | ||
| 2931 | test(utilbool, []) :- | |
| 2932 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/utilbool.pl')). | |
| 2933 | ||
| 2934 | test(util_integer, []) :- | |
| 2935 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/util_integer.pl')). | |
| 2936 | ||
| 2937 | test(modulea, []) :- | |
| 2938 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/modulea.pl')). | |
| 2939 | ||
| 2940 | test(delundoesadd, []) :- | |
| 2941 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/delundoesadd.pl')). | |
| 2942 | ||
| 2943 | test(birthday, []) :- | |
| 2944 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/birthday.pl')). | |
| 2945 | ||
| 2946 | test(trivial_no_solution, []) :- | |
| 2947 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/trivial_no_solution.pl')). | |
| 2948 | ||
| 2949 | test(sets1, []) :- | |
| 2950 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/sets1.pl')). | |
| 2951 | ||
| 2952 | test(sets2, []) :- | |
| 2953 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/sets2.pl')). | |
| 2954 | ||
| 2955 | test(address_book, []) :- | |
| 2956 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/address_book.pl')). | |
| 2957 | ||
| 2958 | test(abstract_memory, []) :- | |
| 2959 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/abstract_memory.pl')). | |
| 2960 | ||
| 2961 | test(cache_memory, []) :- | |
| 2962 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/cache_memory.pl')). | |
| 2963 | ||
| 2964 | test(address_book_3a, []) :- | |
| 2965 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/address_book_3a.pl')). | |
| 2966 | ||
| 2967 | test(overlapping_ranges, []) :- | |
| 2968 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/overlapping_ranges.pl')). | |
| 2969 | ||
| 2970 | test(origin_tracking, []) :- | |
| 2971 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/origin_tracking.pl')). | |
| 2972 | ||
| 2973 | test(java_types, []) :- | |
| 2974 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/java_types.pl')). | |
| 2975 | ||
| 2976 | test(railway, []) :- | |
| 2977 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/railway.pl')). | |
| 2978 | ||
| 2979 | test(syllogism, []) :- | |
| 2980 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/syllogism.pl')). | |
| 2981 | ||
| 2982 | test(chord, []) :- | |
| 2983 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/chord.pl')). | |
| 2984 | ||
| 2985 | test(chord2, []) :- | |
| 2986 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/chord2.pl')). | |
| 2987 | ||
| 2988 | test(chord_bug_model, []) :- | |
| 2989 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/chord_bug_model.pl')). | |
| 2990 | ||
| 2991 | test(mark_sweep_gc, []) :- | |
| 2992 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/mark_sweep_gc.pl')). | |
| 2993 | ||
| 2994 | test(dijkstra_2_process, []) :- | |
| 2995 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/dijkstra_2_process.pl')). | |
| 2996 | ||
| 2997 | test(peterson, []) :- | |
| 2998 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/peterson.pl')). | |
| 2999 | ||
| 3000 | test(genealogy, []) :- | |
| 3001 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/genealogy.pl')). | |
| 3002 | ||
| 3003 | % wrong result for handshake, properties prevent finding a solution, probably caused by translation of 'one sig .. extends Person' | |
| 3004 | test(handshake, []) :- | |
| 3005 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/handshake.pl')). | |
| 3006 | ||
| 3007 | % error when setting up constants; argument of MU expression has more than one element | |
| 3008 | test(send_money, []) :- | |
| 3009 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/send_money.pl')). | |
| 3010 | % same as for send_money | |
| 3011 | test(four_bit_adder, []) :- | |
| 3012 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/4_bit_adder.pl')). | |
| 3013 | ||
| 3014 | test(farmer, []) :- | |
| 3015 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/farmer.pl')). | |
| 3016 | ||
| 3017 | test(ins, []) :- | |
| 3018 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/ins.pl')). | |
| 3019 | ||
| 3020 | test(ring_election1, []) :- | |
| 3021 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/ring_election1.pl')). | |
| 3022 | ||
| 3023 | test(ring_election2, []) :- | |
| 3024 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/ring_election2.pl')). | |
| 3025 | ||
| 3026 | test(com, []) :- | |
| 3027 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/com.pl')). | |
| 3028 | ||
| 3029 | test(paragraph_numbering, []) :- | |
| 3030 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/paragraph_numbering.pl')). | |
| 3031 | ||
| 3032 | %test(mark_sweep_gc2, []) :- | |
| 3033 | % load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/marksweepgc2.pl')). | |
| 3034 | ||
| 3035 | :- end_tests(full_machine_translation). | |
| 3036 | ||
| 3037 | :- endif. | |
| 3038 | % errors | |
| 3039 | /* | |
| 3040 | % translation failed for bijection_relation | |
| 3041 | test(ins_label, []) :- | |
| 3042 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/ins_label.pl')). | |
| 3043 | ||
| 3044 | % unknown identifier X in field while X_Sig exists | |
| 3045 | test(java_map, []) :- | |
| 3046 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/java_map.pl')). | |
| 3047 | % similar as above | |
| 3048 | test(firewire, []) :- | |
| 3049 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/firewire.pl')). | |
| 3050 | ||
| 3051 | % problems with ordering/next | |
| 3052 | test(view_backing, []) :- | |
| 3053 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/view_backing.pl')). | |
| 3054 | % similar as above | |
| 3055 | test(prisoners, []) :- | |
| 3056 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/prisoners.pl')). | |
| 3057 | ||
| 3058 | % missing translation for integer_sum | |
| 3059 | test(messaging, []) :- | |
| 3060 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/messaging.pl')). | |
| 3061 | ||
| 3062 | % Unknown identifier "this" in properties | |
| 3063 | test(hotel, []) :- | |
| 3064 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/hotel.pl')). | |
| 3065 | ||
| 3066 | test(p300_hotel, []) :- | |
| 3067 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/p300_hotel.pl')). | |
| 3068 | ||
| 3069 | test(flip_flop_state, []) :- | |
| 3070 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/flip_flop_state.pl')). | |
| 3071 | ||
| 3072 | test(reset_flip_flop_with_enable, []) :- | |
| 3073 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/reset_flip_flop_with_enable.pl')). | |
| 3074 | ||
| 3075 | % problem new remove this? singleton set problem with this | |
| 3076 | % but also uses unsupported module util/graph | |
| 3077 | test(dijkstra_k_state, []) :- | |
| 3078 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/dijkstra_k_state.pl')). | |
| 3079 | ||
| 3080 | % type errors, e.g., for bool'Not | |
| 3081 | test(ring_orientation, []) :- | |
| 3082 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/ring_orientation.pl')). | |
| 3083 | ||
| 3084 | %! An error occurred (source: type_error) ! | |
| 3085 | %! Type mismatch: Expected (((POW(Board)*INTEGER)*INTEGER)<->Queen), but was ((POW(Board)*INTEGER)<->(INTEGER*Queen)) in 'queens_Board' | |
| 3086 | %! Line: 7 Column: 16 until Line: 7 Column: 16 in file: alloytranslation | |
| 3087 | test(eight_queens, []) :- | |
| 3088 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/8_queens.pl')). | |
| 3089 | ||
| 3090 | % Could not infer type of _universe0 | |
| 3091 | test(java_types_soundness, []) :- | |
| 3092 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/java_types_soundness.pl')). | |
| 3093 | ||
| 3094 | test(sudoku1, []) :- | |
| 3095 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/sudoku1.pl')). | |
| 3096 | ||
| 3097 | test(sequence_test, []) :- | |
| 3098 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/sequence_test.pl')). | |
| 3099 | ||
| 3100 | test(seq_preconditions, []) :- | |
| 3101 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/seq_preconditions.pl')). | |
| 3102 | ||
| 3103 | test(hanoi, []) :- | |
| 3104 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/hanoi.pl')). | |
| 3105 | ||
| 3106 | test(directctrl,[]) :- | |
| 3107 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/directctrl.pl')). | |
| 3108 | ||
| 3109 | test(views,[]) :- | |
| 3110 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/views.pl')). | |
| 3111 | ||
| 3112 | % unsupported iden keyword in "in" | |
| 3113 | test(graphiso, []) :- | |
| 3114 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/graphiso.pl')). | |
| 3115 | ||
| 3116 | test(basic_auth, []) :- | |
| 3117 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/basic_auth.pl')). | |
| 3118 | ||
| 3119 | % Unknown identifier "univ" | |
| 3120 | test(properties, []) :- | |
| 3121 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/properties.pl')). | |
| 3122 | ||
| 3123 | % can probably not be translated due to univ | |
| 3124 | test(iolus, []) :- | |
| 3125 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/iolus.pl')). | |
| 3126 | test(distribution, []) :- | |
| 3127 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/distribution.pl')). | |
| 3128 | */ |