| 1 | % (c) 2017-2026 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_level_inactive_for(19) -> 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_description | |
| 742 | Operation = operation(BPOS,identifier(BPOS,OperationName),[],[],precondition(BPOS,TBody,skip(none))), | |
| 743 | (Functor=check | |
| 744 | -> ajoin(['Counterexample for Alloy check command ',CommandId, ' found'],DescText) | |
| 745 | ; ajoin(['Executed Alloy ',Functor,' command ',CommandId],DescText)), | |
| 746 | DescOp = description_operation(BPOS,description_text(BPOS,DescText),Operation), | |
| 747 | extend_machine_acc(operations, MAcc, DescOp, NewMAcc) % nknown operation nod | |
| 748 | ). | |
| 749 | ||
| 750 | remove_facts_and_assertions_from_list([], []). | |
| 751 | remove_facts_and_assertions_from_list([AlloyTerm|T], NT) :- | |
| 752 | (fact(AlloyTerm); assertion(AlloyTerm)), | |
| 753 | !, | |
| 754 | debug_println(19, remove_facts_and_assertions_from_command), | |
| 755 | remove_facts_and_assertions_from_list(T, NT). | |
| 756 | remove_facts_and_assertions_from_list([AlloyTerm|T], [AlloyTerm|NT]) :- | |
| 757 | remove_facts_and_assertions_from_list(T, NT). | |
| 758 | ||
| 759 | %% remove_facts_and_assertions_from_command(AlloyTerm, NAlloyTerm). | |
| 760 | % Facts and assertions are inlined in Alloy commands by Alloy's parser. | |
| 761 | % We here remove facts and assertions from a command's body since they are translated as machine properties. | |
| 762 | remove_facts_and_assertions_from_command(and(AlloyTerms,APOS), NAlloyConj) :- | |
| 763 | !, | |
| 764 | remove_facts_and_assertions_from_list(AlloyTerms, NAlloyTerms), | |
| 765 | ( NAlloyTerms = [SingleTerm] | |
| 766 | -> NAlloyConj = SingleTerm | |
| 767 | ; NAlloyConj = and(NAlloyTerms,APOS) | |
| 768 | ). | |
| 769 | remove_facts_and_assertions_from_command(AlloyTerm, AlloyTerm). | |
| 770 | ||
| 771 | % We need to remove the negation of assertions stated in a check command when | |
| 772 | % translating to the assertions to prove in AterlierB. | |
| 773 | remove_negations_of_check_command(POS,check, Body, NBody) :- | |
| 774 | Body= and(List,APos), | |
| 775 | remove_negations_of_check_command_list(POS, List, NList), | |
| 776 | NBody = and(NList,APos). | |
| 777 | remove_negations_of_check_command(_, run, Body, Body). | |
| 778 | ||
| 779 | remove_negations_of_check_command_list(_, [], []). | |
| 780 | remove_negations_of_check_command_list(pos(_, CommandCol), [AlloyTerm|T], NList) :- | |
| 781 | get_alloy_position(AlloyTerm, APOS), | |
| 782 | APOS = pos(_, Col), | |
| 783 | Col >= CommandCol, | |
| 784 | % filter those assertions stated in the command (do not remove negations of inlined assertions) | |
| 785 | !, | |
| 786 | remove_negation_alloy_term(AlloyTerm, NewAlloyTerm), | |
| 787 | remove_negations_of_check_command_list(pos(_, CommandCol), T, NT), | |
| 788 | NList = [NewAlloyTerm|NT]. | |
| 789 | remove_negations_of_check_command_list(POS, [AlloyTerm|T], [AlloyTerm|NT]) :- | |
| 790 | remove_negations_of_check_command_list(POS, T, NT). | |
| 791 | ||
| 792 | remove_negation_alloy_term(not(AlloyTerm,_,_), AlloyTerm) :- | |
| 793 | !. | |
| 794 | remove_negation_alloy_term(AlloyTerm, AlloyTerm). | |
| 795 | ||
| 796 | translate_scopes_for_command(Command,SignatureNames,ResPredicate) :- | |
| 797 | get_command_scopes(Command, GlobalScope, ExactScopes, UpBoundScopes, _BitWidth, _CmdMaxSeq), | |
| 798 | maxseq(MaxSeq), | |
| 799 | % global scope, exact scopes and bitwidth | |
| 800 | % We do not need to set the bitwidth since we have real integers in B. | |
| 801 | ResPredicate = conjunct(none,SeqScopePred,conjunct(none,TScopes,TGlobalScopes)), | |
| 802 | % translate exact and upper bound scopes first | |
| 803 | translate_exact_and_upper_bound_scopes(0, ExactScopes, UpBoundScopes, EUSignatureNames, TScopes, OrdSigCounter1), | |
| 804 | % if present, define the global scope for the remaining signatures | |
| 805 | translate_global_scope(OrdSigCounter1, GlobalScope, SignatureNames, EUSignatureNames, TGlobalScopes, _), | |
| 806 | translate_seq_scopes(MaxSeq, SeqScopePred). | |
| 807 | ||
| 808 | translate_seq_scopes(MaxSeq, ScopePred) :- | |
| 809 | findall((Seq,MaxSeq), is_seq(Seq), Seqs), | |
| 810 | maplist(generate_leq_scope_predicate, Seqs, ScopePreds), | |
| 811 | join_predicates(conjunct, ScopePreds, ScopePred). | |
| 812 | ||
| 813 | % no exact scopes defined | |
| 814 | translate_exact_and_upper_bound_scopes(OrdSigCounter, [], [], ExactSigNames, TGlobalScopes, OrdSigCounter) :- | |
| 815 | !, | |
| 816 | ExactSigNames = [], | |
| 817 | TGlobalScopes = truth(none). | |
| 818 | translate_exact_and_upper_bound_scopes(OrdSigCounter, ExactScopes, UpBoundScopes, SignatureNames, TScopes, NewOrdSigCounter) :- | |
| 819 | trans_exact_or_upbnd_scopes(upper, OrdSigCounter, UpBoundScopes, [], UpBoundSigNames, [], TempTUpScopes, OrdSigCnt1), | |
| 820 | trans_exact_or_upbnd_scopes(exact, OrdSigCnt1, ExactScopes, [], ExactSigNames, [], TempTExactScopes, NewOrdSigCounter), | |
| 821 | append(TempTUpScopes, TempTExactScopes, TempTScopes), | |
| 822 | append(ExactSigNames, UpBoundSigNames, SignatureNames), | |
| 823 | join_predicates(conjunct, TempTScopes, TScopes). | |
| 824 | ||
| 825 | trans_exact_or_upbnd_scopes(_, OrdSigCounter, [], NamesAcc, NamesAcc, TScopeAcc, TScopeAcc, OrdSigCounter). | |
| 826 | trans_exact_or_upbnd_scopes(ScopeType, OrdSigCounter, [(SigName,Scope)|T], NameAcc, ExactSigNames, TScopeAcc, TempTExactScopes, NewOrdSigCnt) :- | |
| 827 | is_ordered_signature(SigName), | |
| 828 | !, | |
| 829 | define_ordered_signature_as_integer_set(OrdSigCounter, SigName, Scope, TScope, Cnt1), | |
| 830 | trans_exact_or_upbnd_scopes(ScopeType, Cnt1, T, [SigName|NameAcc], ExactSigNames, [TScope|TScopeAcc], TempTExactScopes, NewOrdSigCnt). | |
| 831 | trans_exact_or_upbnd_scopes(exact, OrdSigCounter, [(SigName,Scope)|T], NameAcc, ExactSigNames, TScopeAcc, TempTExactScopes, NewOrdSigCnt) :- | |
| 832 | generate_exact_scope_predicate((SigName,Scope), TScope), | |
| 833 | trans_exact_or_upbnd_scopes(exact, OrdSigCounter, T, [SigName|NameAcc], ExactSigNames, [TScope|TScopeAcc], TempTExactScopes, NewOrdSigCnt). | |
| 834 | trans_exact_or_upbnd_scopes(upper, OrdSigCounter, [(SigName,Scope)|T], NameAcc, ExactSigNames, TScopeAcc, TempTExactScopes, NewOrdSigCnt) :- | |
| 835 | generate_leq_scope_predicate((SigName,Scope), TScope), | |
| 836 | trans_exact_or_upbnd_scopes(upper, OrdSigCounter, T, [SigName|NameAcc], ExactSigNames, [TScope|TScopeAcc], TempTExactScopes, NewOrdSigCnt). | |
| 837 | ||
| 838 | generate_exact_scope_predicate((SigName,Scope), TScopePred) :- | |
| 839 | translate_e_p(SigName, TSignatureName), | |
| 840 | % debug_format(19,'Exact scope for SignatureName=~w with scope ~w~n',[SigName,Scope]), | |
| 841 | TScopePred = equal(none,card(none,TSignatureName),integer(none,Scope)). | |
| 842 | generate_leq_scope_predicate((SigName,Scope), TScopePred) :- | |
| 843 | translate_e_p(SigName, TSignatureName), | |
| 844 | TScopePred = less_equal(none,card(none,TSignatureName),integer(none,Scope)). | |
| 845 | ||
| 846 | define_ordered_signatures_as_integer_set([], OrdSigCounter, _, [], OrdSigCounter). | |
| 847 | define_ordered_signatures_as_integer_set([TSignatureName|T], OrdSigCounter, Scope, [TScope|TScopes], NewOrdSigCounter) :- | |
| 848 | define_ordered_signature_as_integer_set(OrdSigCounter, TSignatureName, Scope, TScope, OrdSigCounter1), | |
| 849 | define_ordered_signatures_as_integer_set(T, OrdSigCounter1, Scope, TScopes, NewOrdSigCounter). | |
| 850 | ||
| 851 | define_ordered_signature_as_integer_set(OrdSigCounter, TSignatureName, Scope, TScope, NewOrdSigCounter) :- | |
| 852 | NewOrdSigCounter is OrdSigCounter+Scope, | |
| 853 | UpBound is NewOrdSigCounter-1, | |
| 854 | % TSignatureName = OrdSigCounter...UpBound | |
| 855 | TScope = equal(none,identifier(none,TSignatureName), | |
| 856 | interval(none,integer(none,OrdSigCounter),integer(none,UpBound))). | |
| 857 | ||
| 858 | % translate_global_scope(inputCounter,inputGlobalScope,inputSigNames,inputExactSigNames, OutPredicate,OutNewCounter) | |
| 859 | translate_global_scope(OrdSigCounter, -1, _, _, TGlobalScopes, OrdSigCounter) :- | |
| 860 | !, | |
| 861 | TGlobalScopes = truth(none). % no global scope defined | |
| 862 | translate_global_scope(OrdSigCounter, GlobalScope, SignatureNames, ExactSigNames, | |
| 863 | TGlobalScopes, NewOrdSigCounter) :- | |
| 864 | split_ordered_unordered_signatures(SignatureNames, ExactSigNames, OrderedSigNames, RestSignatureNames), | |
| 865 | translate_global_scope_aux(RestSignatureNames, GlobalScope, [], TempTGlobalScopes), | |
| 866 | join_predicates(conjunct, TempTGlobalScopes, TTGlobalScopes), | |
| 867 | % ordered signatures are a subset of integers, OrdSigCounter: from which number on can we assign objects | |
| 868 | define_ordered_signatures_as_integer_set(OrderedSigNames, OrdSigCounter, GlobalScope, TOrderedScopes, NewOrdSigCounter), | |
| 869 | join_predicates(conjunct, [TTGlobalScopes|TOrderedScopes], TGlobalScopes). | |
| 870 | ||
| 871 | translate_global_scope_aux([], _, Acc, Acc). | |
| 872 | translate_global_scope_aux([SignatureName|T], GlobalScope, Acc, TGlobalScopes) :- | |
| 873 | \+ abstract_sig(SignatureName), | |
| 874 | translate_e_p(SignatureName, TSignatureName), | |
| 875 | TScope = less_equal(none,card(none,TSignatureName),integer(none,GlobalScope)), | |
| 876 | translate_global_scope_aux(T, GlobalScope, [TScope|Acc], TGlobalScopes). | |
| 877 | translate_global_scope_aux([_|T], GlobalScope, Acc, TGlobalScopes) :- | |
| 878 | translate_global_scope_aux(T, GlobalScope, Acc, TGlobalScopes). | |
| 879 | ||
| 880 | split_ordered_unordered_signatures(SNames, ExactSNames, OSNames, Rest) :- | |
| 881 | split_ordered_unordered_signatures(SNames, [], [], TOSNames, TRest), | |
| 882 | % remove exact signatures which are defined separately | |
| 883 | subtract(TOSNames, ExactSNames, OSNames), | |
| 884 | subtract(TRest, ExactSNames, Rest). | |
| 885 | ||
| 886 | split_ordered_unordered_signatures([], OAcc, RAcc, OAcc, RAcc). | |
| 887 | split_ordered_unordered_signatures([SName|T], OAcc, RAcc, OSNames, Rest) :- | |
| 888 | is_ordered_signature(SName), | |
| 889 | \+ member(SName, OAcc), | |
| 890 | !, | |
| 891 | split_ordered_unordered_signatures(T, [SName|OAcc], RAcc, OSNames, Rest). | |
| 892 | split_ordered_unordered_signatures([SName|T], OAcc, RAcc, OSNames, Rest) :- | |
| 893 | \+ is_ordered_signature(SName), | |
| 894 | \+ member(SName, RAcc), | |
| 895 | !, | |
| 896 | split_ordered_unordered_signatures(T, OAcc, [SName|RAcc], OSNames, Rest). | |
| 897 | split_ordered_unordered_signatures([_|T], OAcc, RAcc, OSNames, Rest) :- | |
| 898 | split_ordered_unordered_signatures(T, OAcc, RAcc, OSNames, Rest). | |
| 899 | ||
| 900 | % signature in (subset) | |
| 901 | define_sig_as_set_or_constant(MAcc, Name, Options, POS, NewMAcc) :- | |
| 902 | memberchk(subset(Parents), Options), | |
| 903 | !, | |
| 904 | % maplist(assert_extending_signature(Name),Parents) , % subset signatures do not need to be distinct | |
| 905 | translate_pos(POS, BPOS), | |
| 906 | define_sig_as_set_or_constant_aux(constants, MAcc, Name, Options, BPOS, MAcc1), | |
| 907 | % TO DO: consider several parents -> we need the universe type | |
| 908 | Parents = [Parent|_], | |
| 909 | translate_e_p(Name, TName), | |
| 910 | translate_e_p(Parent, TParent), | |
| 911 | TNode = subset(BPOS,TName,TParent), | |
| 912 | extend_machine_acc(properties, MAcc1, TNode, NewMAcc). | |
| 913 | % signature extends | |
| 914 | define_sig_as_set_or_constant(MAcc, Name, Options, POS, NewMAcc) :- | |
| 915 | member(subsig(Parent), Options), | |
| 916 | !, | |
| 917 | ( member(one, Options) -> | |
| 918 | One = one | |
| 919 | ; One = set | |
| 920 | ), | |
| 921 | assert_extending_signature(Name, Parent, One), | |
| 922 | translate_pos(POS, BPOS), | |
| 923 | define_sig_as_set_or_constant_aux(constants, MAcc, Name, Options, BPOS, MAcc1), | |
| 924 | translate_e_p(Name, TName), | |
| 925 | translate_e_p(Parent, TParent), | |
| 926 | TNode = subset(BPOS,TName,TParent), | |
| 927 | extend_machine_acc(properties, MAcc1, TNode, NewMAcc). | |
| 928 | % default signature, but we introduced an artifical parent type, i.e., a deferred set in B | |
| 929 | define_sig_as_set_or_constant(MAcc, Name, Options, POS, NewMAcc) :- | |
| 930 | translate_pos(POS, BPOS), | |
| 931 | artificial_parent_type(Name, ParentId, _), | |
| 932 | !, | |
| 933 | translate_e_p(Name, TName), | |
| 934 | TNode = subset(BPOS,TName,ParentId), | |
| 935 | extend_machine_acc(properties, MAcc, TNode, MAcc1), | |
| 936 | define_sig_as_set_or_constant_aux(constants, MAcc1, Name, Options, BPOS, NewMAcc). | |
| 937 | % default signature | |
| 938 | define_sig_as_set_or_constant(MAcc, Name, Options, POS, NewMAcc) :- | |
| 939 | translate_pos(POS, BPOS), | |
| 940 | define_sig_as_set_or_constant_aux(sets, MAcc, Name, Options, BPOS, NewMAcc). | |
| 941 | ||
| 942 | define_sig_as_set_or_constant_aux(sets, MAcc, Name, Options, BPOS, NewMAcc) :- | |
| 943 | member(one, Options), | |
| 944 | !, | |
| 945 | atom_concat('_', Name, EnumElement), | |
| 946 | % TO DO: couldn't figure out untyped ast of enumerated set, define enumerated set S = {_S} instead of constant etc. | |
| 947 | extend_machine_acc(sets, MAcc, deferred_set(BPOS,Name), MAcc1), | |
| 948 | extend_machine_acc(constants, MAcc1, identifier(BPOS,EnumElement), MAcc2), | |
| 949 | extend_machine_acc(properties, MAcc2, equal(BPOS,identifier(BPOS,Name),set_extension(BPOS,[identifier(BPOS,EnumElement)])), NewMAcc). | |
| 950 | define_sig_as_set_or_constant_aux(sets, MAcc, Name, Options, BPOS, NewMAcc) :- | |
| 951 | member(some, Options), | |
| 952 | !, | |
| 953 | extend_machine_acc(sets, MAcc, deferred_set(BPOS,Name), MAcc1), | |
| 954 | extend_machine_acc(properties, MAcc1, greater_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 | member(lone, Options), | |
| 957 | !, | |
| 958 | extend_machine_acc(sets, MAcc, deferred_set(BPOS,Name), MAcc1), | |
| 959 | extend_machine_acc(properties, MAcc1, less_equal(BPOS,card(BPOS,identifier(BPOS,Name)),integer(BPOS,1)), NewMAcc). | |
| 960 | define_sig_as_set_or_constant_aux(sets, MAcc, Name, _Options, BPOS, NewMAcc) :- | |
| 961 | extend_machine_acc(sets, MAcc, deferred_set(BPOS,Name), NewMAcc). | |
| 962 | define_sig_as_set_or_constant_aux(constants, MAcc, Name, _Options, BPOS, NewMAcc) :- | |
| 963 | extend_machine_acc(constants, MAcc, identifier(BPOS,Name), NewMAcc). | |
| 964 | ||
| 965 | % -------- | |
| 966 | % Semantic translation rules: translate expression or predicate | |
| 967 | % -------- | |
| 968 | translate_e_p2(A, TA) :- %% functor(A,F,N),format('~n TRANSLATE: ~w/~w : ~w ~n',[F,N,A]), | |
| 969 | translate_quantifier_e(A, TA), | |
| 970 | !. | |
| 971 | translate_e_p2(A, TA) :- | |
| 972 | translate_cst_e_p(A, TA), | |
| 973 | !. | |
| 974 | translate_e_p2(A, TA) :- | |
| 975 | translate_unary_e_p(A, TA), | |
| 976 | !. | |
| 977 | translate_e_p2(A, TA) :- | |
| 978 | translate_binary_e_p(A, TA), | |
| 979 | !. | |
| 980 | translate_e_p2(A, TA) :- | |
| 981 | translate_if_then_else(A, TA), | |
| 982 | !. | |
| 983 | translate_e_p2(A, _) :- | |
| 984 | add_error(load_alloy_model, 'Translation failed for:', A), | |
| 985 | fail. | |
| 986 | ||
| 987 | translate_e_p(A, TA) :- | |
| 988 | translate_e_p2(A, TA), | |
| 989 | check_valid_raw_translation(A,TA). | |
| 990 | ||
| 991 | :- load_files(library(system), [when(compile_time), imports([environ/2])]). | |
| 992 | :- if(environ(prob_safe_mode,true)). | |
| 993 | check_valid_raw_translation(A,Raw) :- \+ ground(Raw), | |
| 994 | add_error(alloy2b,'Non-ground raw AST:',Raw,Raw), | |
| 995 | write(A),nl, trace, translate_e_p2(A,_), | |
| 996 | fail. | |
| 997 | :- endif. | |
| 998 | check_valid_raw_translation(_,_). | |
| 999 | % Translation in the context where we expect an integer | |
| 1000 | % This is the E_{int} translation function in the article | |
| 1001 | % The following rule is not necessary: untyped_b_ast_to_integer will peel off set extensions | |
| 1002 | %translate_e_p_integer(identifier(ID,_Type,POS), identifier(BPOS,ID)) :- %Type=integer, ? | |
| 1003 | % is_singleton_set(ID),!, | |
| 1004 | % translate_pos(POS, BPOS). | |
| 1005 | translate_e_p_integer(integer(A,POS), integer(BPOS,A)) :- | |
| 1006 | !, | |
| 1007 | translate_pos(POS, BPOS). | |
| 1008 | translate_e_p_integer(A, BAstInt) :- | |
| 1009 | translate_e_p(A, BAst), | |
| 1010 | untyped_b_ast_to_integer(BAst, BAstInt). | |
| 1011 | ||
| 1012 | untyped_b_ast_to_integer(integer(BPOS,A), integer(BPOS,A)) :- | |
| 1013 | !. | |
| 1014 | untyped_b_ast_to_integer(set_extension(_,[Single]), Single) :- | |
| 1015 | !. | |
| 1016 | % Alloy sums the elements of sets of integers so we can use SIGMA which also strips singleton sets like the MU operator. | |
| 1017 | % If preference alloy_strict_integers is set, we only accept singleton sets as integers and throw a WD error otherwise. | |
| 1018 | untyped_b_ast_to_integer(BAst, BAstInt) :- | |
| 1019 | get_preference(alloy_strict_integers, Strict), | |
| 1020 | Strict == false, | |
| 1021 | !, | |
| 1022 | get_b_position(BAst, BPOS), | |
| 1023 | check_position(BPOS,untyped_b_ast_to_integer), | |
| 1024 | BAstInt = general_sum(BPOS,[identifier(BPOS,z)],member(BPOS,identifier(BPOS,z),BAst),identifier(BPOS,z)). | |
| 1025 | untyped_b_ast_to_integer(BAst, BAstInt) :- | |
| 1026 | get_b_position(BAst, BPOS), | |
| 1027 | check_position(BPOS,untyped_b_ast_to_integer), | |
| 1028 | BAstInt = mu(BPOS,BAst). | |
| 1029 | ||
| 1030 | ||
| 1031 | ||
| 1032 | % Translation in the context where we expect a singleton set. | |
| 1033 | % Otherwise, a well-definedness error is thrown. | |
| 1034 | % This is the E_{one} translation function in the article. | |
| 1035 | % Note that the arguments are already translated (using \semE{.} in the article). | |
| 1036 | translate_e_p_one(set_extension(_,[One]), Res) :- | |
| 1037 | !, | |
| 1038 | Res = One. | |
| 1039 | translate_e_p_one(BAst, mu(none,BAst)). | |
| 1040 | ||
| 1041 | % construct_choose(TSetA,external_function_call(none,'CHOOSE',[TSetA],string(none,'a member of X'),TypeParams,Decl)) :- | |
| 1042 | % % format of raw AST of CHOOSE copied from btype2 | |
| 1043 | % TypeParams = rewrite_protected([identifier(none,T)]), | |
| 1044 | % Decl = rewrite_protected(total_function(none,pow_subset(none,identifier(none,T)),identifier(none,T))). | |
| 1045 | translate_if_then_else(if_then_else(ConditionPred,TruthExpr,FalsityExpr,_Type,POS), TIfThenElse) :- | |
| 1046 | translate_e_p(ConditionPred, TConditionPred), | |
| 1047 | translate_e_p(TruthExpr, TTruthExpr), | |
| 1048 | translate_e_p(FalsityExpr, TFalsityExpr), | |
| 1049 | translate_pos(POS, BPOS), | |
| 1050 | get_type_and_arity_from_alloy_term(TruthExpr, Type, _), | |
| 1051 | ( ( Type = [untyped] | |
| 1052 | ; is_primitive_type(Type, _) | |
| 1053 | ) | |
| 1054 | -> | |
| 1055 | TIfThenElse = conjunct(BPOS, | |
| 1056 | implication(BPOS,TConditionPred,TTruthExpr), | |
| 1057 | implication(BPOS,negation(BPOS,TConditionPred),TFalsityExpr)) | |
| 1058 | ; TIfThenElse = if_then_else(BPOS,TConditionPred,TTruthExpr,TFalsityExpr) | |
| 1059 | ). | |
| 1060 | ||
| 1061 | translate_quantifier_e(Quantifier, TQuantifier) :- | |
| 1062 | Quantifier =.. [Functor,Params,Fields,Body,_Type,POS], | |
| 1063 | member(Functor, [all,no,some,one,lone,comprehension]), | |
| 1064 | maplist(translate_e_p, Params, TParams), | |
| 1065 | maplist(strip_singleton_set, TParams, TTParams), % strip singleton sets for parameter definition in the untyped B ast (only identifier/2 nodes allowed in there) | |
| 1066 | translate_pos(POS, BPOS), | |
| 1067 | maplist(translate_quantifier_field, Fields, TFieldsList, SingletonSetNames), | |
| 1068 | ( is_disjoint_quantifier(Fields) | |
| 1069 | -> | |
| 1070 | maplist(translate_e_p, SingletonSetNames, TSets), % TSets are the translated Fields | |
| 1071 | % encoding all_different by union(Set1,Set2,) | |
| 1072 | length(Fields, Len), | |
| 1073 | construct_all_diff(BPOS,Len,TSets, AllDiff), | |
| 1074 | join_untyped_ast_nodes(conjunct, [AllDiff|TFieldsList], TFields) | |
| 1075 | ; join_untyped_ast_nodes(conjunct, TFieldsList, TFields) | |
| 1076 | ), | |
| 1077 | translate_e_p(Body, TBody), | |
| 1078 | translate_quantifier_e_aux(BPOS, Functor, TTParams, TFields, TBody, TQuantifier), | |
| 1079 | % TO DO: retract singleton sets introduced in quantifiers on exit | |
| 1080 | maplist(retract_singleton_set(BPOS), SingletonSetNames). | |
| 1081 | ||
| 1082 | construct_all_diff(BPOS,2,[S1,S2],AllDiff) :- !, AllDiff = not_equal(BPOS,S1,S2). | |
| 1083 | construct_all_diff(BPOS,Len,TSets, AllDiff) :- | |
| 1084 | AllDiff = equal(BPOS,card(BPOS,general_union(BPOS,set_extension(BPOS,TSets))),integer(BPOS,Len)). | |
| 1085 | % encoding all_different by card(union({O1,O2,...,Ok}) = k | |
| 1086 | ||
| 1087 | ||
| 1088 | translate_quantifier_e_aux(Pos, all, TParams, TFields, TBody, forall(Pos,TParams,implication(Pos,TFields,TBody))). | |
| 1089 | translate_quantifier_e_aux(Pos, no, TParams, TFields, TBody, negation(Pos,exists(Pos,TParams,conjunct(Pos,TFields,TBody)))). | |
| 1090 | translate_quantifier_e_aux(Pos, some, TParams, TFields, TBody, exists(Pos,TParams,conjunct(Pos,TFields,TBody))). | |
| 1091 | translate_quantifier_e_aux(Pos, one, TParams, TFields, TBody, equal(Pos,card(Pos,comprehension_set(Pos,TParams,conjunct(Pos,TFields,TBody))),integer(Pos,1))). | |
| 1092 | 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))). | |
| 1093 | translate_quantifier_e_aux(Pos, comprehension, TParams, TFields, TBody, comprehension_set(Pos,TParams,conjunct(Pos,TFields,TBody))). | |
| 1094 | ||
| 1095 | % Translate Constants | |
| 1096 | translate_cst_e_p(iden(POS), event_b_identity(BPOS)) :- % has no Span Info ! | |
| 1097 | translate_pos(POS, BPOS). | |
| 1098 | translate_cst_e_p(identifier(Cst,_,POS), BConstruct) :- | |
| 1099 | alloy_constant_to_b(Cst, BPOS, BConstruct), | |
| 1100 | !, | |
| 1101 | translate_pos(POS, BPOS). | |
| 1102 | translate_cst_e_p(none(POS), TNone) :- | |
| 1103 | !, | |
| 1104 | translate_pos(POS, BPOS), | |
| 1105 | TNone = empty_set(BPOS). | |
| 1106 | translate_cst_e_p(this, _) :- | |
| 1107 | print('this not yet translated'), | |
| 1108 | nl, | |
| 1109 | fail. | |
| 1110 | ||
| 1111 | ||
| 1112 | alloy_constant_to_b(none, BPOS, empty_set(BPOS)). | |
| 1113 | alloy_constant_to_b('boolean''False', BPOS, boolean_false(BPOS)). | |
| 1114 | alloy_constant_to_b('boolean''True', BPOS, boolean_true(BPOS)). | |
| 1115 | alloy_constant_to_b('boolean''Bool', BPOS, bool_set(BPOS)). | |
| 1116 | ||
| 1117 | translate_unary_e_p(cast2int(Expr,_Type,POS), Result) :- | |
| 1118 | !, | |
| 1119 | translate_pos(POS, BPOS), | |
| 1120 | translate_e_p_integer(Expr, TExpr), | |
| 1121 | Result = set_extension(BPOS, [TExpr]). | |
| 1122 | translate_unary_e_p(cast2sigint(Expr,_Type,_Pos), Result) :- | |
| 1123 | % TO DO: do we need this? how is this written in Alloy? | |
| 1124 | !, | |
| 1125 | translate_e_p(Expr, TExpr), | |
| 1126 | Result = TExpr. | |
| 1127 | translate_unary_e_p(string(StringCodes,POS), Result) :- | |
| 1128 | atom_codes(String, StringCodes), | |
| 1129 | !, | |
| 1130 | translate_pos(POS, BPOS), | |
| 1131 | Result = set_extension(BPOS,[string(BPOS,String)]). | |
| 1132 | translate_unary_e_p(seq(ID), Result) :- | |
| 1133 | translate_unary_e_p(ID, TID), | |
| 1134 | !, | |
| 1135 | Result = sequence_extension(none,TID). | |
| 1136 | translate_unary_e_p(Int, Result) :- | |
| 1137 | integer(Int), % Note: this is not really a unary operator but a constant | |
| 1138 | !, | |
| 1139 | Result = integer(none,Int). | |
| 1140 | translate_unary_e_p(Term, Result) :- | |
| 1141 | ( Term = identifier(ID,type(TypeList,_),POS), | |
| 1142 | TypeList = [SigName|_] | |
| 1143 | ; Term = ID, | |
| 1144 | POS = none | |
| 1145 | ), | |
| 1146 | atom(ID), | |
| 1147 | sig_field_id(ID, SigName), | |
| 1148 | !, | |
| 1149 | atom_concat(ID, '_', NID), | |
| 1150 | atom_concat(NID, SigName, NNID), | |
| 1151 | translate_pos(POS, BPOS), | |
| 1152 | (is_singleton_set_id(NNID) | |
| 1153 | -> Result = set_extension(BPOS,[identifier(BPOS,NNID)]) | |
| 1154 | ; Result = identifier(BPOS,NNID)). | |
| 1155 | translate_unary_e_p(identifier(ID,Type,POS), Result) :- | |
| 1156 | prepend_identifier_of_module_import(ID, Type, NID), | |
| 1157 | % singleton enumerated set like S = {_S} | |
| 1158 | enumerated_set(NID), | |
| 1159 | is_singleton_set_id(NID), | |
| 1160 | !, | |
| 1161 | translate_pos(POS, BPOS), | |
| 1162 | Result = set_extension(BPOS,[identifier(BPOS,NID)]). | |
| 1163 | translate_unary_e_p(identifier(ID,Type,POS), Result) :- | |
| 1164 | prepend_identifier_of_module_import(ID, Type, NID), | |
| 1165 | is_singleton_set_id(NID), | |
| 1166 | !, | |
| 1167 | translate_pos(POS, BPOS), | |
| 1168 | Result = set_extension(BPOS,[identifier(BPOS,NID)]). | |
| 1169 | translate_unary_e_p(ID, Result) :- | |
| 1170 | atom(ID), | |
| 1171 | prepend_module_name(ID,NID), | |
| 1172 | enumerated_set(NID), | |
| 1173 | is_singleton_set_id(NID), | |
| 1174 | !, | |
| 1175 | Result = set_extension(none,[identifier(none,NID)]). | |
| 1176 | translate_unary_e_p(ID, Result) :- | |
| 1177 | atom(ID), | |
| 1178 | prepend_module_name(ID,NID), | |
| 1179 | is_singleton_set_id(NID), | |
| 1180 | !, | |
| 1181 | Result = set_extension(none,[identifier(none,NID)]). | |
| 1182 | translate_unary_e_p(integer(A,POS), Result) :- | |
| 1183 | !, | |
| 1184 | translate_pos(POS, BPOS), | |
| 1185 | Result = set_extension(BPOS,[integer(BPOS,A)]). | |
| 1186 | translate_unary_e_p(identifier('Int',_Type,POS), Result) :- | |
| 1187 | !, | |
| 1188 | translate_pos(POS, BPOS), | |
| 1189 | integer_type(IntOrInteger), | |
| 1190 | Result = integer_set(BPOS,IntOrInteger). | |
| 1191 | translate_unary_e_p(identifier(Id,_Type,POS), Result) :- | |
| 1192 | alloy_natural_id(Id, 'Natural'), | |
| 1193 | !, | |
| 1194 | translate_pos(POS, BPOS), | |
| 1195 | natural_type(NatOrNatural), | |
| 1196 | Result = integer_set(BPOS,NatOrNatural). | |
| 1197 | translate_unary_e_p(identifier(Id,_Type,POS), Result) :- | |
| 1198 | alloy_natural_id(Id, 'One'), | |
| 1199 | !, | |
| 1200 | translate_pos(POS, BPOS), | |
| 1201 | Result = set_extension(BPOS,[integer(BPOS,1)]). | |
| 1202 | translate_unary_e_p(identifier(Id,_Type,POS), Result) :- | |
| 1203 | alloy_natural_id(Id, 'Zero'), | |
| 1204 | !, | |
| 1205 | translate_pos(POS, BPOS), | |
| 1206 | Result = set_extension(BPOS,[integer(BPOS,0)]). | |
| 1207 | translate_unary_e_p(identifier('String',_,_), Result) :- | |
| 1208 | !, | |
| 1209 | Result = string_set(none). | |
| 1210 | translate_unary_e_p(identifier(ID,Type,POS), Result) :- | |
| 1211 | !, | |
| 1212 | prepend_identifier_of_module_import(ID, Type, NID), | |
| 1213 | translate_pos(POS, BPOS), | |
| 1214 | Result = identifier(BPOS,NID). | |
| 1215 | translate_unary_e_p('Int', Result) :- | |
| 1216 | !, | |
| 1217 | integer_type(IntOrInteger), | |
| 1218 | Result = integer_set(none,IntOrInteger). | |
| 1219 | translate_unary_e_p(Id, Result) :- | |
| 1220 | alloy_natural_id(Id, 'Natural'), | |
| 1221 | !, | |
| 1222 | natural_type(NatOrNatural), | |
| 1223 | Result = integer_set(none,NatOrNatural). | |
| 1224 | translate_unary_e_p(Id, Result) :- | |
| 1225 | alloy_natural_id(Id, 'One'), | |
| 1226 | !, | |
| 1227 | Result = set_extension(none,[integer(none,1)]). | |
| 1228 | translate_unary_e_p(Id, Result) :- | |
| 1229 | alloy_natural_id(Id, 'Zero'), | |
| 1230 | !, | |
| 1231 | Result = set_extension(none,[integer(none,0)]). | |
| 1232 | translate_unary_e_p(boolean(true,POS), Result) :- | |
| 1233 | !, % was boolean_true, but Alloy has no booleans | |
| 1234 | translate_pos(POS, BPOS), | |
| 1235 | Result = truth(BPOS). | |
| 1236 | translate_unary_e_p(boolean(false,POS), Result) :- | |
| 1237 | !, % was boolean_false | |
| 1238 | translate_pos(POS, BPOS), | |
| 1239 | Result = falsity(BPOS). | |
| 1240 | translate_unary_e_p(Type, Result) :- | |
| 1241 | % lhs of sequence is integer, Alloy Types are like [seqInt,A] for set(couple(INTEGER,A)) | |
| 1242 | atom(Type), | |
| 1243 | atom_prefix(seq, Type), | |
| 1244 | !, | |
| 1245 | integer_type(IntOrInteger), | |
| 1246 | Result = integer_set(none,IntOrInteger). | |
| 1247 | translate_unary_e_p(ID, Result) :- | |
| 1248 | atom(ID), | |
| 1249 | prepend_module_name(ID,NID), | |
| 1250 | !, | |
| 1251 | Result = identifier(none,NID). | |
| 1252 | translate_unary_e_p(UnaryP, TUnaryP) :- | |
| 1253 | % and/or defines a list of ast nodes | |
| 1254 | UnaryP =.. [Op,ArgList|_], | |
| 1255 | memberchk(Op, [and,or]), % translated to conjunct/disjunct | |
| 1256 | is_list(ArgList), | |
| 1257 | !, | |
| 1258 | maplist(translate_e_p, ArgList, TArgList), | |
| 1259 | join_predicates(Op, TArgList, TUnaryP). | |
| 1260 | translate_unary_e_p(UnaryP, TUnaryP) :- | |
| 1261 | UnaryP =.. [Op,Arg,_Type,POS], | |
| 1262 | member(Op, [no,one,some,lone,exactlyof,oneof,someof,loneof]), | |
| 1263 | !, | |
| 1264 | translate_e_p(Arg, TArg), | |
| 1265 | translate_pos(POS, BPOS), | |
| 1266 | translate_quantified_e(BPOS, Op, TArg, TUnaryP). | |
| 1267 | translate_unary_e_p(card(Arg,_Type,POS), set_extension(BPOS,[card(BPOS,TArg)])) :- | |
| 1268 | !, | |
| 1269 | translate_e_p(Arg, TArg), | |
| 1270 | translate_pos(POS, BPOS). | |
| 1271 | translate_unary_e_p(UnaryP, TUnaryP) :- | |
| 1272 | UnaryP =.. [Op,Arg,_Type,POS], | |
| 1273 | translate_e_p(Arg, TArg), | |
| 1274 | alloy_to_b_unary_operator(Op, BOp), | |
| 1275 | translate_pos(POS, BPOS), | |
| 1276 | TUnaryP =.. [BOp,BPOS,TArg]. | |
| 1277 | ||
| 1278 | alloy_natural_id(Id, Suffix) :- | |
| 1279 | atom(Id), | |
| 1280 | module_in_scope_but_root('util''natural', Alias), | |
| 1281 | atom_concat(Alias, '\'', Prefix), | |
| 1282 | atom_concat(Prefix, Suffix, Id). | |
| 1283 | ||
| 1284 | % support for Alloy modules to maintain unique identifiers | |
| 1285 | prepend_module_name(ID,NID) :- | |
| 1286 | atom(ID), | |
| 1287 | \+ has_module_prefix(ID), | |
| 1288 | current_module_in_scope(ModuleName), | |
| 1289 | !, | |
| 1290 | atom_concat(ModuleName, '''', ModuleNameP), | |
| 1291 | atom_concat(ModuleNameP, ID, NID). | |
| 1292 | prepend_module_name(ID,ID). | |
| 1293 | ||
| 1294 | has_module_prefix(ID) :- | |
| 1295 | atom(ID), | |
| 1296 | module_in_scope_but_root(ModuleName, Alias), | |
| 1297 | ( atom_prefix(ModuleName , ID) | |
| 1298 | ; Alias \== 'alloy2b_none', | |
| 1299 | atom_prefix(Alias, ID) | |
| 1300 | ), | |
| 1301 | !. | |
| 1302 | ||
| 1303 | prepend_identifier_of_module_import(ID, Type, NID) :- | |
| 1304 | % field names of signatures from imported modules are not unique, | |
| 1305 | % their type (the signature name) is unique though | |
| 1306 | atom(ID), | |
| 1307 | Type = type([Inner|_],_), | |
| 1308 | module_in_scope_but_root(ModuleName, Alias), | |
| 1309 | ( Alias \== 'alloy2b_none' | |
| 1310 | -> Name = Alias | |
| 1311 | ; Name = ModuleName | |
| 1312 | ), | |
| 1313 | atom_prefix(Name, Inner), | |
| 1314 | atom_concat(Name, '''', NameP), | |
| 1315 | \+ atom_prefix(NameP, ID), | |
| 1316 | !, | |
| 1317 | atom_concat(NameP, ID, NID). | |
| 1318 | prepend_identifier_of_module_import(ID, _, ID). | |
| 1319 | ||
| 1320 | %% FUNCTIONS defined by func in util: | |
| 1321 | % alloy_to_b_natural_utility_function(Name, BPOS, Params, Result). | |
| 1322 | % Special cases with no direct counterpart in B. | |
| 1323 | alloy_to_b_natural_utility_function('''ord''first', BPOS, [], set_extension(BPOS,[integer(BPOS,0)])). | |
| 1324 | alloy_to_b_natural_utility_function('''ord''last', BPOS, [], set_extension(BPOS,[max_int(BPOS)])). | |
| 1325 | alloy_to_b_natural_utility_function('''ord''next', BPOS, [P1Int], set_extension(BPOS,[add(BPOS,P1Int,integer(BPOS,1))])). | |
| 1326 | alloy_to_b_natural_utility_function('''ord''prev', BPOS, [P1Int], set_extension(BPOS,[minus(BPOS,P1Int,integer(BPOS,1))])). | |
| 1327 | alloy_to_b_natural_utility_function('''One', BPOS, [], set_extension(BPOS,[integer(BPOS,1)])). | |
| 1328 | alloy_to_b_natural_utility_function('''Zero', BPOS, [], set_extension(BPOS,[integer(BPOS,0)])). | |
| 1329 | alloy_to_b_natural_utility_function('''min', BPOS, [], set_extension(BPOS,[max(BPOS,set_extension(BPOS,[integer(BPOS,0),min_int(BPOS)]))])). | |
| 1330 | alloy_to_b_natural_utility_function('''inc', BPOS, [P1Int], set_extension(BPOS,[add(BPOS,P1Int,integer(BPOS,1))])). | |
| 1331 | alloy_to_b_natural_utility_function('''dec', BPOS, [P1Int], set_extension(BPOS,[minus(BPOS,P1Int,integer(BPOS,1))])). | |
| 1332 | ||
| 1333 | % alloy_to_b_integer_utility_function(Name, BPOS, Params, Result). | |
| 1334 | % Special cases with no direct counterpart in B. | |
| 1335 | alloy_to_b_integer_utility_function('''signum', BPOS, [P1Int], Result) :- | |
| 1336 | !, | |
| 1337 | % IF int(p) < 0 THEN -1 ELSE IF int(p) > 0 THEN 1 ELSE 0 END END | |
| 1338 | 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)]))). | |
| 1339 | alloy_to_b_integer_utility_function('''zero', BPOS, [P1Int], Result) :- | |
| 1340 | !, | |
| 1341 | % int(p) = 0 | |
| 1342 | Result = equal(BPOS,P1Int,integer(BPOS,0)). | |
| 1343 | alloy_to_b_integer_utility_function(Name, BPOS, [P1Int], Result) :- | |
| 1344 | ( Name == '''pos', BOp = greater | |
| 1345 | ; Name == '''neg', BOp = less), | |
| 1346 | !, | |
| 1347 | translate_e_p_integer(P1Int, P1Int), | |
| 1348 | % int(p) > 0 or int(p) < 0 | |
| 1349 | Result =.. [BOp,BPOS,P1Int,integer(BPOS,0)]. | |
| 1350 | alloy_to_b_integer_utility_function(Name, BPOS, [P1Int], Result) :- | |
| 1351 | ( Name == '''nonpos', BOp = less_equal | |
| 1352 | ; Name == '''nonneg', BOp = greater_equal), | |
| 1353 | !, | |
| 1354 | translate_e_p_integer(P1Int, P1Int), | |
| 1355 | % int(p) <= 0 or int(p) >= 0 | |
| 1356 | Result =.. [BOp,BPOS,P1Int,integer(BPOS,0)]. | |
| 1357 | alloy_to_b_integer_utility_function(Name, BPOS, [P1Int,P2Int], Result) :- | |
| 1358 | ( Name == '''smaller', BOp = min | |
| 1359 | ; Name == '''larger', BOp = max), | |
| 1360 | !, | |
| 1361 | % {min({int(p1),int(p2)})} or {max({int(p1),int(p2)})} | |
| 1362 | Inner =.. [BOp,BPOS,set_extension(BPOS,[P1Int,P2Int])], | |
| 1363 | Result = set_extension(BPOS,[Inner]). | |
| 1364 | alloy_to_b_integer_utility_function(Name, BPOS, [P1Int], Result) :- | |
| 1365 | ( Name == '''nexts', BOp = greater | |
| 1366 | ; Name == '''prevs', BOp = less), | |
| 1367 | !, | |
| 1368 | % {x | x : INTEGER & x > int(p)} or {x | x : INTEGER & x < int(p)} | |
| 1369 | Inner =.. [BOp,BPOS,identifier(BPOS,x),P1Int], | |
| 1370 | integer_type(IntOrInteger), | |
| 1371 | check_position(BPOS,alloy_to_b_integer_utility_function(Name)), | |
| 1372 | Result = comprehension_set(BPOS,[identifier(BPOS,x)], | |
| 1373 | conjunct(BPOS,member(BPOS,identifier(BPOS,x),integer_set(none,IntOrInteger)),Inner)). | |
| 1374 | ||
| 1375 | %% alloy_to_b_integer_natural_utility_func(Name,Arity,BOperator,ArgType,ReturnType). | |
| 1376 | % Special cases with direct counterparts in B. | |
| 1377 | alloy_to_b_integer_natural_utility_func(FunName, Arity, BOp, ArgType, ReturnType) :- | |
| 1378 | is_util_integer_natural_func(FunName, _, AlloyOp), | |
| 1379 | ( alloy_to_b_integer_func(AlloyOp, Arity, BOp, ArgType, ReturnType) | |
| 1380 | ; alloy_to_b_integer_operator_func(AlloyOp, Arity, BOp, ArgType, ReturnType) | |
| 1381 | ; alloy_to_b_integer_to_integer_func(AlloyOp, Arity, BOp, ArgType, ReturnType) | |
| 1382 | ; alloy_to_b_operator_func(AlloyOp, Arity, BOp, ArgType, ReturnType) | |
| 1383 | ),!. | |
| 1384 | ||
| 1385 | is_util_integer_natural_func(FunName, UtilType, AlloyOp) :- | |
| 1386 | atom(FunName), | |
| 1387 | module_in_scope_but_root(ModuleName, Alias), | |
| 1388 | atom(ModuleName), | |
| 1389 | atom(Alias), | |
| 1390 | ( atom_concat(ModuleName, AlloyOp, FunName) | |
| 1391 | ; atom_concat(Alias, AlloyOp, FunName) | |
| 1392 | ), | |
| 1393 | ( ModuleName == 'util''integer', | |
| 1394 | UtilType = integer | |
| 1395 | ; ModuleName == 'util''natural', | |
| 1396 | UtilType = natural | |
| 1397 | ). | |
| 1398 | ||
| 1399 | % functions with integer arguments and result | |
| 1400 | alloy_to_b_integer_to_integer_func('''minus', 2, minus, integer, integer). | |
| 1401 | alloy_to_b_integer_to_integer_func('''plus', 2, add, integer, integer). | |
| 1402 | alloy_to_b_integer_to_integer_func('''div', 2, div, integer, integer). | |
| 1403 | alloy_to_b_integer_to_integer_func('''mul', 2, multiplication, integer, integer). | |
| 1404 | alloy_to_b_integer_to_integer_func('''rem', 2, modulo, integer, integer). | |
| 1405 | % alloy_to_b_integer_to_integer_func('''sum',sigma, integer, integer). % TO DO: translate sum | |
| 1406 | alloy_to_b_integer_to_integer_func('''add', 2, add, integer, integer). | |
| 1407 | alloy_to_b_integer_to_integer_func('''sub', 2, minus, integer, integer). | |
| 1408 | % Unary: | |
| 1409 | alloy_to_b_integer_to_integer_func('''negate', 1, unary_minus, integer, integer). | |
| 1410 | 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 | |
| 1411 | alloy_to_b_integer_to_integer_func('''prev', 1, predecessor, integer, integer). | |
| 1412 | ||
| 1413 | % functions with integer result but set arguments | |
| 1414 | alloy_to_b_integer_func('''min', 1, min, set, integer). | |
| 1415 | alloy_to_b_integer_func('''max', 1, max, set, integer). | |
| 1416 | alloy_to_b_integer_func('''min', 0, min_int, set, integer). % TO DO: investigate bit-width related translation | |
| 1417 | alloy_to_b_integer_func('''max', 0, max_int, set, integer). | |
| 1418 | % Note: for run Arithmetic for 6 Int the Alloy Evaluator produces {-32} for min and {+31} for max | |
| 1419 | % predicate functions with integer arguments | |
| 1420 | alloy_to_b_operator_func('''next', 0, successor, set, set). | |
| 1421 | alloy_to_b_operator_func('''prev', 0, predecessor, set, set). | |
| 1422 | ||
| 1423 | % predicate functions with integer arguments | |
| 1424 | alloy_to_b_integer_operator_func('''gt', 2, greater, integer, set). | |
| 1425 | alloy_to_b_integer_operator_func('''lt', 2, less, integer, set). | |
| 1426 | alloy_to_b_integer_operator_func('''gte', 2, greater_equal, integer, set). | |
| 1427 | alloy_to_b_integer_operator_func('''lte', 2, less_equal, integer, set). | |
| 1428 | alloy_to_b_integer_operator_func('''eq', 2, equal, integer, set). | |
| 1429 | ||
| 1430 | % Not[b] = bool(b = FALSE) | |
| 1431 | alloy_to_b_boolean_utility_function('boolean''Not', [TP1], BPOS, Result) :- | |
| 1432 | !, | |
| 1433 | Result = convert_bool(BPOS,equal(BPOS,TP1,boolean_false(BPOS))). | |
| 1434 | alloy_to_b_boolean_utility_function('boolean''isTrue', [TP1], BPOS, Result) :- | |
| 1435 | !, | |
| 1436 | Result = equal(BPOS,TP1,boolean_true(BPOS)). | |
| 1437 | alloy_to_b_boolean_utility_function('boolean''isFalse', [TP1], BPOS, Result) :- | |
| 1438 | !, | |
| 1439 | Result = equal(BPOS,TP1,boolean_false(BPOS)). | |
| 1440 | % And[a,b] = bool(a = TRUE & b = TRUE) | |
| 1441 | alloy_to_b_boolean_utility_function('boolean''And', [TP1,TP2], BPOS, Result) :- | |
| 1442 | !, | |
| 1443 | Result = convert_bool(BPOS,conjunct(BPOS,equal(BPOS,TP1,boolean_true(BPOS)),equal(BPOS,TP2,boolean_true(BPOS)))). | |
| 1444 | % Or[a,b] = bool(a = TRUE or b = TRUE) | |
| 1445 | alloy_to_b_boolean_utility_function('boolean''Or', [TP1,TP2], BPOS, Result) :- | |
| 1446 | !, | |
| 1447 | Result = convert_bool(BPOS,disjunct(BPOS,equal(BPOS,TP1,boolean_true(BPOS)),equal(BPOS,TP2,boolean_true(BPOS)))). | |
| 1448 | % Nand[a,b] = bool(a = FALSE or b = FALSE) | |
| 1449 | alloy_to_b_boolean_utility_function('boolean''Nand', [TP1,TP2], BPOS, Result) :- | |
| 1450 | !, | |
| 1451 | Result = convert_bool(BPOS,disjunct(BPOS,equal(BPOS,TP1,boolean_false(BPOS)),equal(BPOS,TP2,boolean_false(BPOS)))). | |
| 1452 | % Nor[a,b] = bool(a = FALSE & b = FALSE) | |
| 1453 | alloy_to_b_boolean_utility_function('boolean''Nor', [TP1,TP2], BPOS, Result) :- | |
| 1454 | !, | |
| 1455 | Result = convert_bool(BPOS,conjunct(BPOS,equal(BPOS,TP1,boolean_false(BPOS)),equal(BPOS,TP2,boolean_false(BPOS)))). | |
| 1456 | % Xor[a,b] = bool((a = FALSE & b = TRUE) or (a = TRUE & b = FALSE)) | |
| 1457 | alloy_to_b_boolean_utility_function('boolean''Xor', [TP1,TP2], BPOS, Result) :- | |
| 1458 | !, | |
| 1459 | LHS = conjunct(BPOS,equal(BPOS,TP1,boolean_false(BPOS)),equal(BPOS,TP2,boolean_true(BPOS))), | |
| 1460 | RHS = conjunct(BPOS,equal(BPOS,TP1,boolean_true(BPOS)),equal(BPOS,TP2,boolean_false(BPOS))), | |
| 1461 | Result = convert_bool(BPOS,disjunct(BPOS,LHS,RHS)). | |
| 1462 | alloy_to_b_boolean_utility_function(FunName, _, BPOS, truth(BPOS)) :- | |
| 1463 | atom_prefix('boolean', FunName), | |
| 1464 | !, | |
| 1465 | add_error(alloy_to_b_boolean_utility_function, 'Function from util/boolean currently not supported', [], BPOS). | |
| 1466 | ||
| 1467 | % dom[r] = dom(r) | |
| 1468 | alloy_to_b_relational_utility_function(UtilFunName, [TRelation], BPOS, TCall) :- | |
| 1469 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1470 | atom_concat(RelationAlias, '\'dom', UtilFunName), | |
| 1471 | !, | |
| 1472 | TCall = domain(BPOS,TRelation). | |
| 1473 | % ran[r] = ran(r) | |
| 1474 | alloy_to_b_relational_utility_function(UtilFunName, [TRelation], BPOS, TCall) :- | |
| 1475 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1476 | atom_concat(RelationAlias, '\'ran', UtilFunName), | |
| 1477 | !, | |
| 1478 | TCall = range(BPOS,TRelation). | |
| 1479 | % total[r,d] = !x.(x:d => r[{x}] /= {}}) | |
| 1480 | alloy_to_b_relational_utility_function(UtilFunName, [TRelation,TDomain], BPOS, TCall) :- | |
| 1481 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1482 | atom_concat(RelationAlias, '\'total', UtilFunName), | |
| 1483 | !, | |
| 1484 | ID0 = identifier(BPOS,x), | |
| 1485 | LHS = member(BPOS,ID0,TDomain), | |
| 1486 | RHS = not_equal(BPOS,image(BPOS,TRelation,set_extension(BPOS,[ID0])),empty_set(BPOS)), | |
| 1487 | TCall = forall(BPOS,[ID0],implication(BPOS,LHS,RHS)). | |
| 1488 | % functional[r,d] = !x.(x:d => card(r[{x}]) <= 1) | |
| 1489 | alloy_to_b_relational_utility_function(UtilFunName, [TRelation,TDomain], BPOS, TCall) :- | |
| 1490 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1491 | atom_concat(RelationAlias, '\'functional', UtilFunName), | |
| 1492 | !, | |
| 1493 | ID0 = identifier(BPOS,x), | |
| 1494 | LHS = member(BPOS,ID0,TDomain), | |
| 1495 | RHS = less_equal(BPOS,card(BPOS,image(BPOS,TRelation,set_extension(BPOS,[ID0]))),integer(BPOS,1)), | |
| 1496 | TCall = forall(BPOS,[ID0],implication(BPOS,LHS,RHS)). | |
| 1497 | % function[r,d] = !x.(x:d => card(r[{x}]) = 1) | |
| 1498 | alloy_to_b_relational_utility_function(UtilFunName, [TRelation,TDomain], BPOS, TCall) :- | |
| 1499 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1500 | atom_concat(RelationAlias, '\'function', UtilFunName), | |
| 1501 | !, | |
| 1502 | ID0 = identifier(BPOS,x), | |
| 1503 | LHS = member(BPOS,ID0,TDomain), | |
| 1504 | RHS = equal(BPOS,card(BPOS,image(BPOS,TRelation,set_extension(BPOS,[ID0]))),integer(BPOS,1)), | |
| 1505 | TCall = forall(BPOS,[ID0],implication(BPOS,LHS,RHS)). | |
| 1506 | % injective[r,c] = !(y).(y:c => card(r~[{y}]) <= 1) | |
| 1507 | alloy_to_b_relational_utility_function(UtilFunName, [TRelation,TCodomain], BPOS, TCall) :- | |
| 1508 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1509 | atom_concat(RelationAlias, '\'injective', UtilFunName), | |
| 1510 | !, | |
| 1511 | ID0 = identifier(BPOS,y), | |
| 1512 | LHS = member(BPOS,ID0,TCodomain), | |
| 1513 | RHS = less_equal(BPOS,card(BPOS,image(BPOS,reverse(BPOS,TRelation),set_extension(BPOS,[ID0]))),integer(BPOS,1)), | |
| 1514 | TCall = forall(BPOS,[ID0],implication(BPOS,LHS,RHS)). | |
| 1515 | % surjective[r,c] = !(y).(y:c => r~[{y}] /= {}) | |
| 1516 | alloy_to_b_relational_utility_function(UtilFunName, [TRelation,TCodomain], BPOS, TCall) :- | |
| 1517 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1518 | atom_concat(RelationAlias, '\'surjective', UtilFunName), | |
| 1519 | !, | |
| 1520 | ID0 = identifier(BPOS,y), | |
| 1521 | LHS = member(BPOS,ID0,TCodomain), | |
| 1522 | RHS = not_equal(BPOS,image(BPOS,reverse(BPOS,TRelation),set_extension(BPOS,[ID0])),empty_set(BPOS)), | |
| 1523 | TCall = forall(BPOS,[ID0],implication(BPOS,LHS,RHS)). | |
| 1524 | % bijective[r,c] = !(y).(y:c => card(r~[{y}]) = 1) | |
| 1525 | alloy_to_b_relational_utility_function(UtilFunName, [TRelation,TCodomain], BPOS, TCall) :- | |
| 1526 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1527 | atom_concat(RelationAlias, '\'bijective', UtilFunName), | |
| 1528 | !, | |
| 1529 | ID0 = identifier(BPOS,y), | |
| 1530 | LHS = member(BPOS,ID0,TCodomain), | |
| 1531 | RHS = equal(BPOS,card(BPOS,image(BPOS,reverse(BPOS,TRelation),set_extension(BPOS,[ID0]))),integer(BPOS,1)), | |
| 1532 | TCall = forall(BPOS,[ID0],implication(BPOS,LHS,RHS)). | |
| 1533 | % bijection[r,d,c] = function[r,d] & bijective[r,c] | |
| 1534 | alloy_to_b_relational_utility_function(UtilFunName, [Relation,Domain,Codomain], BPOS, TCall) :- | |
| 1535 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1536 | atom_concat(RelationAlias, '\'bijection', UtilFunName), | |
| 1537 | !, | |
| 1538 | atom_concat(RelationAlias, '\'function', Function), | |
| 1539 | atom_concat(RelationAlias, '\'bijective', Bijective), | |
| 1540 | alloy_to_b_relational_utility_function(Function, [Relation,Domain], BPOS, IsFunction), | |
| 1541 | alloy_to_b_relational_utility_function(Bijective, [Relation,Codomain], BPOS, IsBijective), | |
| 1542 | TCall = conjunct(BPOS,IsFunction,IsBijective). | |
| 1543 | % reflexive[r,s] = id(s) <: r | |
| 1544 | alloy_to_b_relational_utility_function(UtilFunName, [TRelation1,TRelation2], BPOS, TCall) :- | |
| 1545 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1546 | atom_concat(RelationAlias, '\'reflexive', UtilFunName), | |
| 1547 | !, | |
| 1548 | TCall = subset(BPOS,identity(BPOS,TRelation2),TRelation1). | |
| 1549 | % irreflexive[r] = id(dom(r)) /\ r = {} | |
| 1550 | alloy_to_b_relational_utility_function(UtilFunName, [TRelation], BPOS, TCall) :- | |
| 1551 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1552 | atom_concat(RelationAlias, '\'irreflexive', UtilFunName), | |
| 1553 | !, | |
| 1554 | TCall = equal(BPOS,intersection(BPOS,identity(BPOS,domain(BPOS,TRelation)),TRelation),empty_set(BPOS)). | |
| 1555 | % symmetric[r] = r~ <: r | |
| 1556 | alloy_to_b_relational_utility_function(UtilFunName, [TRelation], BPOS, TCall) :- | |
| 1557 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1558 | atom_concat(RelationAlias, '\'symmetric', UtilFunName), | |
| 1559 | !, | |
| 1560 | TCall = subset(BPOS,reverse(BPOS,TRelation),TRelation). | |
| 1561 | % antisymmetric[r] = (r~ /\ r) <: id(dom(r)) | |
| 1562 | alloy_to_b_relational_utility_function(UtilFunName, [TRelation], BPOS, TCall) :- | |
| 1563 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1564 | atom_concat(RelationAlias, '\'antisymmetric', UtilFunName), | |
| 1565 | !, | |
| 1566 | Intersection = intersection(BPOS,reverse(BPOS,TRelation),TRelation), | |
| 1567 | TCall = subset(BPOS,Intersection,identity(BPOS,domain(BPOS,TRelation))). | |
| 1568 | % transitive[r] = (r ; r) <: r | |
| 1569 | alloy_to_b_relational_utility_function(UtilFunName, [TRelation], BPOS, TCall) :- | |
| 1570 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1571 | atom_concat(RelationAlias, '\'transitive', UtilFunName), | |
| 1572 | !, | |
| 1573 | TCall = subset(BPOS,composition(BPOS,TRelation,TRelation),TRelation). | |
| 1574 | % acyclic[r,s] = !x.(x:s => x|->x /: closure1(r)) | |
| 1575 | alloy_to_b_relational_utility_function(UtilFunName, [TRelation1,TRelation2], BPOS, TCall) :- | |
| 1576 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1577 | atom_concat(RelationAlias, '\'acyclic', UtilFunName), | |
| 1578 | !, | |
| 1579 | ID0 = identifier(BPOS,x), | |
| 1580 | TCall = forall(BPOS,[ID0],implication(BPOS,member(BPOS,ID0,TRelation2), | |
| 1581 | not_member(BPOS,couple(BPOS,ID0,ID0),closure(BPOS,TRelation1)))). | |
| 1582 | % complete[r,s] = !(x,y).(x:s & y:s & x /= y => x|->y : (r \/ r~)) | |
| 1583 | alloy_to_b_relational_utility_function(UtilFunName, [TRelation1,TRelation2], BPOS, TCall) :- | |
| 1584 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1585 | atom_concat(RelationAlias, '\'complete', UtilFunName), | |
| 1586 | !, | |
| 1587 | ID0 = identifier(BPOS,x), | |
| 1588 | ID1 = identifier(BPOS,y), | |
| 1589 | LHS = conjunct(BPOS,conjunct(BPOS,member(BPOS,ID0,TRelation2),member(BPOS,ID1,TRelation2)),not_equal(BPOS,ID0,ID1)), | |
| 1590 | RHS = member(BPOS,couple(BPOS,ID0,ID1),union(BPOS,TRelation1,reverse(BPOS,TRelation1))), | |
| 1591 | TCall = forall(BPOS,[ID0,ID1],implication(BPOS,LHS,RHS)). | |
| 1592 | % preorder[r,s] = reflexive[r,s] & transitive[r] | |
| 1593 | alloy_to_b_relational_utility_function(UtilFunName, [Relation1,Relation2], BPOS, TCall) :- | |
| 1594 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1595 | atom_concat(RelationAlias, '\'preorder', UtilFunName), | |
| 1596 | !, | |
| 1597 | atom_concat(RelationAlias, '\'reflexive', Reflexive), | |
| 1598 | atom_concat(RelationAlias, '\'transitive', Transitive), | |
| 1599 | alloy_to_b_relational_utility_function(Reflexive, [Relation1,Relation2], BPOS, IsReflexive), | |
| 1600 | alloy_to_b_relational_utility_function(Transitive, [Relation1], BPOS, IsTransitive), | |
| 1601 | TCall = conjunct(BPOS,IsReflexive,IsTransitive). | |
| 1602 | % equivalence[r,s] = preorder[r,s] & symmetric[r] | |
| 1603 | alloy_to_b_relational_utility_function(UtilFunName, [Relation1,Relation2], BPOS, TCall) :- | |
| 1604 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1605 | atom_concat(RelationAlias, '\'equivalence', UtilFunName), | |
| 1606 | !, | |
| 1607 | atom_concat(RelationAlias, '\'preorder', Preorder), | |
| 1608 | atom_concat(RelationAlias, '\'symmetric', Symmetric), | |
| 1609 | alloy_to_b_relational_utility_function(Preorder, [Relation1,Relation2], BPOS, IsReflexive), | |
| 1610 | alloy_to_b_relational_utility_function(Symmetric, [Relation1], BPOS, IsTransitive), | |
| 1611 | TCall = conjunct(BPOS,IsReflexive,IsTransitive). | |
| 1612 | % partialOrder[r,s] = preorder[r,s] & antisymmetric[r] | |
| 1613 | alloy_to_b_relational_utility_function(UtilFunName, [Relation1,Relation2], BPOS, TCall) :- | |
| 1614 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1615 | atom_concat(RelationAlias, '\'partialOrder', UtilFunName), | |
| 1616 | !, | |
| 1617 | atom_concat(RelationAlias, '\'preorder', Preorder), | |
| 1618 | atom_concat(RelationAlias, '\'antisymmetric', Antisymmetric), | |
| 1619 | alloy_to_b_relational_utility_function(Preorder, [Relation1,Relation2], BPOS, IsReflexive), | |
| 1620 | alloy_to_b_relational_utility_function(Antisymmetric, [Relation1], BPOS, IsTransitive), | |
| 1621 | TCall = conjunct(BPOS,IsReflexive,IsTransitive). | |
| 1622 | % totalOrder[r,s] = partialOrder[r,s] & complete[r,s] | |
| 1623 | alloy_to_b_relational_utility_function(UtilFunName, [Relation1,Relation2], BPOS, TCall) :- | |
| 1624 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1625 | atom_concat(RelationAlias, '\'totalOrder', UtilFunName), | |
| 1626 | !, | |
| 1627 | atom_concat(RelationAlias, '\'partialOrder', Partialorder), | |
| 1628 | atom_concat(RelationAlias, '\'complete', Complete), | |
| 1629 | alloy_to_b_relational_utility_function(Partialorder, [Relation1,Relation2], BPOS, IsReflexive), | |
| 1630 | alloy_to_b_relational_utility_function(Complete, [Relation1,Relation2], BPOS, IsTransitive), | |
| 1631 | TCall = conjunct(BPOS,IsReflexive,IsTransitive). | |
| 1632 | alloy_to_b_relational_utility_function(FunName, _, BPOS, truth(BPOS)) :- | |
| 1633 | module_in_scope_but_root('util\'relation', RelationAlias), | |
| 1634 | atom_prefix(RelationAlias, FunName), | |
| 1635 | !, | |
| 1636 | add_error(alloy_to_b_relational_utility_function, 'Function from util/relation currently not supported', [], BPOS). | |
| 1637 | ||
| 1638 | % remove_prime(Old,New) :- atom_codes(Old,OldC) , delete(OldC,39,NewC) , atom_codes(New,NewC). | |
| 1639 | get_clean_ordering_fun_name(OrderingFunctionName, CleanOrdFunName) :- | |
| 1640 | member(CleanOrdFunName, [first,last,min,max,next,nexts,prev,prevs,larger,smaller,lt,lte,gt,gte]), | |
| 1641 | atom_suffix(CleanOrdFunName, OrderingFunctionName). | |
| 1642 | ||
| 1643 | get_ordering_definition_name(TempFunctionName, SignatureName, FunctionName) :- | |
| 1644 | member(TempFunctionName, [next,prev,nexts,prevs]), | |
| 1645 | atom_concat(TempFunctionName, '_', TTempFunctionName), | |
| 1646 | atom_concat(TTempFunctionName, SignatureName, FunctionName). | |
| 1647 | ||
| 1648 | translate_binary_e_p(in(Arg1,Arg2,_Type,POS), Translation) :- | |
| 1649 | !, | |
| 1650 | translate_pos(POS, BPOS), | |
| 1651 | translate_e_p(Arg1, TArg1), | |
| 1652 | translate_binary_in(TArg1, Arg2, BPOS, Translation). | |
| 1653 | translate_binary_e_p(CartTerm, TCartesian) :- | |
| 1654 | is_cartesian_product_term(CartTerm, Arg1, Arg2, POS), | |
| 1655 | !, | |
| 1656 | translate_pos(POS, BPOS), | |
| 1657 | translate_cartesian(BPOS, Arg1, Arg2, TCartesian). | |
| 1658 | % S <: Rel --> {x1,..,xk| x1:S & (x1,...,xk):Rel} | |
| 1659 | translate_binary_e_p(dom_restr(Arg1,Arg2,_Type,POS), TDom) :- | |
| 1660 | \+ is_binary_relation(Arg2), % for binary relation translation to B domain_restriction works | |
| 1661 | !, | |
| 1662 | get_type_and_arity_from_alloy_term(Arg2, _, Arity), | |
| 1663 | gen_ids_and_couple(Arity, IDS, Couple), | |
| 1664 | translate_pos(POS, BPOS), | |
| 1665 | TDom = comprehension_set(BPOS,IDS,conjunct(BPOS,Mem1,Mem2)), | |
| 1666 | IDS = [ID1|_], | |
| 1667 | check_position(BPOS,translate_binary_e_p), | |
| 1668 | Mem1 = member(BPOS,ID1,TArg1), | |
| 1669 | Mem2 = member(BPOS,Couple,TArg2), | |
| 1670 | translate_e_p(Arg1, TArg1), | |
| 1671 | translate_e_p(Arg2, TArg2). | |
| 1672 | translate_binary_e_p(join(Arg1,Arg2,_,_), TJoin) :- | |
| 1673 | % special case for join with unary ordering definition call such as 'this.(prev + next)' | |
| 1674 | % improves performance to translate to 'this.prev + this.next' | |
| 1675 | annotate_undefined_ordering_definition_call(Arg2, Arg1, NArg2), | |
| 1676 | Arg2 \== NArg2, | |
| 1677 | !, | |
| 1678 | translate_e_p(NArg2, TJoin). | |
| 1679 | translate_binary_e_p(join(Arg1,Arg2,_,_), TJoin) :- | |
| 1680 | % see above clause | |
| 1681 | annotate_undefined_ordering_definition_call(Arg1, Arg2, NArg1), | |
| 1682 | Arg1 \== NArg1, | |
| 1683 | !, | |
| 1684 | translate_e_p(NArg1, TJoin). | |
| 1685 | translate_binary_e_p(join(Arg1,Arg2,_Type,POS), TJoin) :- | |
| 1686 | !, | |
| 1687 | translate_pos(POS, BPOS), | |
| 1688 | translate_join(BPOS, Arg1, Arg2, TJoin). | |
| 1689 | translate_binary_e_p(let(VarName,Expr,Sub,Type,POS), TLet) :- | |
| 1690 | !, | |
| 1691 | translate_e_p(VarName, TVarName), | |
| 1692 | translate_e_p(Expr, TExpr), | |
| 1693 | ( Type == type(['PrimitiveBoolean'],0) -> | |
| 1694 | NewFunctor = let_predicate | |
| 1695 | ; NewFunctor = let_expression | |
| 1696 | ), | |
| 1697 | translate_e_p(Sub, TSub), | |
| 1698 | translate_pos(POS, BPOS), | |
| 1699 | TLet =.. [NewFunctor,BPOS,[TVarName],equal(BPOS,TVarName,TExpr),TSub]. | |
| 1700 | translate_binary_e_p(Call, TCall) :- | |
| 1701 | Call =.. [Functor,Name,Params,Type,POS], | |
| 1702 | ( Functor = pred_call | |
| 1703 | ; Functor = fun_call | |
| 1704 | ), | |
| 1705 | !, | |
| 1706 | translate_pos(POS, BPOS), | |
| 1707 | translate_function_call(Name, Params, Type, BPOS, TCall). | |
| 1708 | translate_binary_e_p(Binary, TBinary) :- | |
| 1709 | Binary =.. [Op,Arg1,Arg2,_Type,POS], | |
| 1710 | alloy_to_b_integer_operator(Op, BOp), | |
| 1711 | !, | |
| 1712 | translate_e_p_integer(Arg1, TArg1), | |
| 1713 | translate_e_p_integer(Arg2, TArg2), | |
| 1714 | translate_pos(POS, BPOS), | |
| 1715 | TBinary =.. [BOp,BPOS,TArg1,TArg2]. | |
| 1716 | translate_binary_e_p(Binary, TBinary) :- | |
| 1717 | Binary =.. [Op,Arg1,Arg2,_Type,POS], | |
| 1718 | \+ add_error_for_univ_or_iden(translate_binary_e_p, Op, Arg1, Arg2), | |
| 1719 | alloy_to_b_binary_operator(Op, BOp), | |
| 1720 | translate_e_p(Arg1, TArg1), | |
| 1721 | translate_e_p(Arg2, TArg2), | |
| 1722 | translate_pos(POS, BPOS), | |
| 1723 | TBinary =.. [BOp,BPOS,TArg1,TArg2]. | |
| 1724 | ||
| 1725 | % We do not allow keywords univ or iden for specific operators which we cannot translate to | |
| 1726 | % an equivalent B expression without introducing the universal type. | |
| 1727 | binary_op_not_allowing_iden_or_univ(equal). | |
| 1728 | binary_op_not_allowing_iden_or_univ(not_equal). | |
| 1729 | binary_op_not_allowing_iden_or_univ(in). | |
| 1730 | binary_op_not_allowing_iden_or_univ(not_in). | |
| 1731 | ||
| 1732 | add_error_for_univ_or_iden(Src, Op, Arg1, Arg2) :- | |
| 1733 | binary_op_not_allowing_iden_or_univ(Op), | |
| 1734 | ( ground(Arg1), | |
| 1735 | is_iden(Arg1) | |
| 1736 | ; ground(Arg2), | |
| 1737 | is_iden(Arg2) | |
| 1738 | ), | |
| 1739 | atom_concat('iden keyword in Alloy operator ', Op, Msg), | |
| 1740 | add_error_not_supported(Src, Msg). | |
| 1741 | add_error_for_univ_or_iden(Src, Op, Arg1, Arg2) :- | |
| 1742 | binary_op_not_allowing_iden_or_univ(Op), | |
| 1743 | ( ground(Arg1), | |
| 1744 | is_univ(Arg1) | |
| 1745 | ; ground(Arg2), | |
| 1746 | is_univ(Arg2) | |
| 1747 | ), | |
| 1748 | atom_concat('univ keyword in Alloy operator ', Op, Msg), | |
| 1749 | add_error_not_supported(Src, Msg). | |
| 1750 | ||
| 1751 | add_error_not_supported(Src, NotSupported) :- | |
| 1752 | atom(NotSupported), | |
| 1753 | add_error(Src, 'Expression not supported by our translation: ', [NotSupported]). | |
| 1754 | ||
| 1755 | translate_binary_in(TArg1, Arg2, _, _) :- | |
| 1756 | add_error_for_univ_or_iden(translate_binary_in, in, TArg1, Arg2), | |
| 1757 | !. | |
| 1758 | % translate TArg1 in Arg2 (multplicities are not allowed for not in) | |
| 1759 | translate_binary_in(TArg1, Mult, BPOS, Translation) :- | |
| 1760 | compound(Mult), | |
| 1761 | functor(Mult, AlloyFunctor, 4), % binary operator with type and pos info | |
| 1762 | alloy_to_b_special_multiplicity_type(AlloyFunctor, _, _, _, _, _, _, _), % TO DO: clean up | |
| 1763 | arg(1, Mult, MDom), | |
| 1764 | arg(2, Mult, MRan), | |
| 1765 | translate_e_p(MDom, TMDom), | |
| 1766 | translate_e_p(MRan, TMRan), | |
| 1767 | alloy_to_b_special_multiplicity_type(AlloyFunctor, BPOS, TArg1, TMDom, TMRan, TMult, AdditionalConstraint, UseInverse), | |
| 1768 | !, | |
| 1769 | ( UseInverse == yes | |
| 1770 | -> TTArg1 = reverse(BPOS,TArg1) | |
| 1771 | ; TTArg1 = TArg1 | |
| 1772 | ), | |
| 1773 | ( AdditionalConstraint == none | |
| 1774 | -> Translation = member(BPOS,TTArg1,TMult) % use element of rather than subset for special type operators | |
| 1775 | ; Translation = conjunct(BPOS,member(BPOS,TTArg1,TMult),AdditionalConstraint) | |
| 1776 | ). | |
| 1777 | % cartesian | |
| 1778 | translate_binary_in(TArg1, Arg2, BPOS, subset(BPOS,TArg1,TArg2)) :- | |
| 1779 | translate_e_p(Arg2, TArg2). | |
| 1780 | ||
| 1781 | % translate expressions of the form Arg1 MULT -> MULT Arg2 with MULT : {some,lone, one, ''} | |
| 1782 | % The result is to be used in member(Pos,LHS,TBinary) not for subset checks ! | |
| 1783 | translate_special_field_multiplicity_binary_e_p(Binary, TBinary) :- | |
| 1784 | Binary =.. [AlloyFunctor,Arg1,Arg2,_Type,POS], | |
| 1785 | translate_pos(POS, BPOS), | |
| 1786 | translate_e_p(Arg1, TArg1), | |
| 1787 | translate_e_p(Arg2, TArg2), | |
| 1788 | % some functions of alloy_to_b_special_multiplicity_type/8 do not apply to | |
| 1789 | % field multiplicities as only one multiplicity is allowed there | |
| 1790 | alloy_to_b_special_multiplicity_type(AlloyFunctor, BPOS, _, TArg1, TArg2, TBinary, _, _WasNo). | |
| 1791 | ||
| 1792 | % Alloy: r in T -> some U | |
| 1793 | % B: r : T <-> U & dom(r)=T | |
| 1794 | alloy_to_b_special_multiplicity_type(total_relation, BPOS, TRel, TMDom, TMRan, relations(BPOS,TMDom,TMRan), AdditionalConstraint, no) :- | |
| 1795 | AdditionalConstraint = equal(BPOS,domain(BPOS,TRel),TMDom). | |
| 1796 | % Alloy: r in T -> one U | |
| 1797 | % B: r : T --> U | |
| 1798 | alloy_to_b_special_multiplicity_type(total_function, BPOS, _, TMDom, TMRan, total_function(BPOS,TMDom,TMRan), none, no). | |
| 1799 | % Alloy: r in T -> lone U | |
| 1800 | % B: r : T +-> U | |
| 1801 | alloy_to_b_special_multiplicity_type(partial_function, BPOS, _, TMDom, TMRan, partial_function(BPOS,TMDom,TMRan), none, no). | |
| 1802 | % Alloy: r in T some -> U | |
| 1803 | % B: r : T <-> U & ran(r) = U | |
| 1804 | alloy_to_b_special_multiplicity_type(surjection_relation, BPOS, TRel, TMDom, TMRan, relations(BPOS,TMDom,TMRan), AdditionalConstraint, no) :- | |
| 1805 | AdditionalConstraint = equal(BPOS,range(BPOS,TRel),TMRan). | |
| 1806 | % Alloy: r in T some -> some U | |
| 1807 | % B: r : T <-> U & dom(r)=T & ran(r) = U | |
| 1808 | alloy_to_b_special_multiplicity_type(total_surjection_relation, BPOS, TRel, TMDom, TMRan, relations(BPOS,TMDom,TMRan), AdditionalConstraint, no) :- | |
| 1809 | AdditionalConstraint = conjunct(BPOS,equal(BPOS,domain(BPOS,TRel),TMDom),equal(BPOS,range(BPOS,TRel),TMRan)). | |
| 1810 | % Alloy: r in T some -> lone U | |
| 1811 | % B: r : T +->> U | |
| 1812 | alloy_to_b_special_multiplicity_type(partial_surjection, BPOS, _, TMDom, TMRan, partial_surjection(BPOS,TMDom,TMRan), none, no). | |
| 1813 | % Alloy: r in T some -> one U | |
| 1814 | % B: r : T -->> U | |
| 1815 | alloy_to_b_special_multiplicity_type(total_surjection, BPOS, _, TMDom, TMRan, total_surjection(BPOS,TMDom,TMRan), none, no). | |
| 1816 | % Alloy: r in T lone -> U | |
| 1817 | % B: r~ : U +-> T | |
| 1818 | alloy_to_b_special_multiplicity_type(injection_relation, BPOS, _, TMDom, TMRan, partial_function(BPOS,TMRan,TMDom), none, yes). | |
| 1819 | % Alloy: r in T lone -> some U | |
| 1820 | % B: r~ : U +->> T | |
| 1821 | alloy_to_b_special_multiplicity_type(injection_surjection_relation, BPOS, _, TMDom, TMRan, partial_surjection(BPOS,TMRan,TMDom), none, yes). | |
| 1822 | % Alloy: r in T lone -> lone U | |
| 1823 | % B: r : T >+> U | |
| 1824 | alloy_to_b_special_multiplicity_type(partial_injection, BPOS, _, TMDom, TMRan, partial_injection(BPOS,TMDom,TMRan), none, no). | |
| 1825 | % Alloy: r in T lone -> one U | |
| 1826 | % B: r : T >-> U | |
| 1827 | alloy_to_b_special_multiplicity_type(total_injection, BPOS, _, TMDom, TMRan, total_injection(BPOS,TMDom,TMRan), none, no). | |
| 1828 | % Alloy: r in T one -> U | |
| 1829 | % B: r~ : U --> T | |
| 1830 | alloy_to_b_special_multiplicity_type(bijection_relation, BPOS, _, TMDom, TMRan, total_function(BPOS,TMRan,TMDom), none, yes). | |
| 1831 | % Alloy: r in T one -> some U | |
| 1832 | % B: r~ : U -->> T | |
| 1833 | alloy_to_b_special_multiplicity_type(total_bijection_relation, BPOS, _, TMDom, TMRan, total_surjection(BPOS,TMRan,TMDom), none, yes). | |
| 1834 | % Alloy: r in T one -> lone U | |
| 1835 | % B: r : T >+>> U | |
| 1836 | alloy_to_b_special_multiplicity_type(partial_bijection, BPOS, _, TMDom, TMRan, partial_bijection(BPOS,TMDom,TMRan), none, no). | |
| 1837 | % Alloy: r in T one -> one U | |
| 1838 | % B: r : T >->> U | |
| 1839 | alloy_to_b_special_multiplicity_type(total_bijection, BPOS, _, TMDom, TMRan, total_bijection(BPOS,TMDom,TMRan), none, no). | |
| 1840 | ||
| 1841 | % Note: Sequences in B are indexed from 1 to n, in Alloy from 0 to n-1. | |
| 1842 | % We do not use B sequences when translating from Alloy but define a partial function with domain 0..n-1 | |
| 1843 | % (we have to manually implement most functions anyway) | |
| 1844 | % Documentation available at http://alloytools.org/quickguide/seq.html | |
| 1845 | %% Sequence function calls without a parameter but the sequence itself. | |
| 1846 | % first: seq[{0}] | |
| 1847 | sequence_function_to_b('seq\'first', BPOS, [Seq], image(BPOS,Seq,set_extension(BPOS,[integer(BPOS,0)]))). | |
| 1848 | % last: seq[{card(seq)-1}] | |
| 1849 | sequence_function_to_b('seq\'last', BPOS, [Seq], image(BPOS,Seq,set_extension(BPOS,[minus(BPOS,card(BPOS,Seq),integer(BPOS,1))]))). | |
| 1850 | % rest: IF seq = <> THEN <> ELSE %x.(x:0..card(seq)-2 | seq(x+1) END | |
| 1851 | 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)))))). | |
| 1852 | % elems: ran(seq) | |
| 1853 | sequence_function_to_b('seq\'elems', BPOS, [Seq], range(BPOS,Seq)). | |
| 1854 | % butlast: seq[{card(seq)-2}] | |
| 1855 | sequence_function_to_b('seq\'butlast', BPOS, [Seq], image(BPOS,Seq,set_extension(BPOS,[minus(BPOS,card(BPOS,Seq),integer(BPOS,2))]))). | |
| 1856 | % isEmpty: seq = <> | |
| 1857 | sequence_function_to_b('seq\'isEmpty', BPOS, [Seq], equal(BPOS,Seq,empty_sequence(BPOS))). | |
| 1858 | % hasDups: card(seq) /= card(ran(seq)) | |
| 1859 | sequence_function_to_b('seq\'hasDups', BPOS, [Seq], not_equal(BPOS,card(BPOS,Seq),card(BPOS,range(BPOS,Seq)))). | |
| 1860 | % inds: 0..card(seq)-1 | |
| 1861 | sequence_function_to_b('seq\'inds', BPOS, [Seq], interval(BPOS,integer(BPOS,0),minus(BPOS,card(BPOS,Seq),integer(BPOS,1)))). | |
| 1862 | % lastIdx: {card(seq)-1} /\ 0..(card(seq)-1) | |
| 1863 | 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))))). | |
| 1864 | % afterLastIdx: {card(seq)} /\ 0..(MAXSEQ-1) | |
| 1865 | 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))))) :- | |
| 1866 | maxseq(MaxSeq). | |
| 1867 | %% Sequence function calls with one parameter and the sequence itself. | |
| 1868 | % idxOf[X]: IF seq~[{E_{one}(X)}] /= {} THEN {min(seq~[{E_{one}(X)}])} ELSE {} END | |
| 1869 | 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))) :- | |
| 1870 | translate_e_p_one(P1, P1One). | |
| 1871 | % lastIdxOf[X]: IF seq~[{E_{one}(X)}] /= {} THEN {max(seq~[{E_{one}(X)}])} ELSE {} END | |
| 1872 | 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))) :- | |
| 1873 | translate_e_p_one(P1, P1One). | |
| 1874 | % indsOf[X]: seq~[{E_{one}(X)}] | |
| 1875 | sequence_function_to_b('seq\'indsOf', BPOS, [Seq,P1], image(BPOS,reverse(BPOS,Seq),set_extension(BPOS,[P1One]))) :- | |
| 1876 | translate_e_p_one(P1, P1One). | |
| 1877 | % append[seq2]: (0..(MAXSEQ-1)) <| (seq \/ %x.(x:card(seq)..(card(seq)+card(seq2)-1) | seq2(x-card(seq)))) | |
| 1878 | 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))))))) :- | |
| 1879 | maxseq(MaxSeq). | |
| 1880 | % Throw WD error if X is not singleton. | |
| 1881 | % add[X]: IF card(seq) < MAXSEQ THEN seq \/ {card(seq) |-> E_{one}(X)} ELSE seq END | |
| 1882 | 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)) :- | |
| 1883 | maxseq(MaxSeq), | |
| 1884 | translate_e_p_one(P1, P1One). | |
| 1885 | % 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 | |
| 1886 | 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)) :- | |
| 1887 | untyped_b_ast_to_integer(P1, P1Int). | |
| 1888 | % Throw WD error if X is not singleton. | |
| 1889 | % setAt[i,X]: IF (i >= 0 & i <= card(seq) ) THEN seq <+ {i |-> E_{one}(X)} ELSE seq END | |
| 1890 | 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)) :- | |
| 1891 | untyped_b_ast_to_integer(P1, P1Int), | |
| 1892 | translate_e_p_one(P2, P2One). | |
| 1893 | % Throw WD error if X is not singleton. | |
| 1894 | % special case for i=0 | |
| 1895 | % insert[0,X]: 0..(m-1) <| {0 |-> E_{one}(X)} \/ %z.(z:1..card(seq) ∧ (z-1):dom(seq) | seq(z-1))) | |
| 1896 | 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))))))) :- | |
| 1897 | untyped_b_ast_to_integer(P1, P1Int), | |
| 1898 | P1Int = integer(_,0), | |
| 1899 | maxseq(MaxSeq), | |
| 1900 | translate_e_p_one(P2, P2One). | |
| 1901 | % 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))) | |
| 1902 | 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))))))) :- | |
| 1903 | P1 \= integer(_,0), | |
| 1904 | maxseq(MaxSeq), | |
| 1905 | untyped_b_ast_to_integer(P1, P1Int), | |
| 1906 | translate_e_p_one(P2, P2One). | |
| 1907 | % 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 | |
| 1908 | 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))) :- | |
| 1909 | untyped_b_ast_to_integer(P1, P1Int), | |
| 1910 | untyped_b_ast_to_integer(P2, P2Int). | |
| 1911 | sequence_function_to_b(FunName, BPOS, _, Res) :- | |
| 1912 | atom_prefix('seq', FunName), | |
| 1913 | !, | |
| 1914 | add_error(sequence_function_to_b, 'Function from util/sequences currently not supported', [], BPOS), | |
| 1915 | Res = truth(BPOS). | |
| 1916 | ||
| 1917 | translate_seq_function_param(join(identifier(this,type([Type],1),IPos),Arg2,JType,JPos), TParam) :- | |
| 1918 | !, | |
| 1919 | % remove join with this for signature fields | |
| 1920 | translate_e_p(join(identifier(Type,type([Type],1),IPos),Arg2,JType,JPos), TTParam), | |
| 1921 | TParam = TTParam. | |
| 1922 | translate_seq_function_param(Param, TParam) :- | |
| 1923 | translate_e_p(Param, TParam). | |
| 1924 | ||
| 1925 | % Translation of operations from utility libraries | |
| 1926 | % util/sequence | |
| 1927 | translate_function_call(Function, Params, _Type, BPOS, TCall) :- | |
| 1928 | maplist(translate_seq_function_param, Params, TParams), | |
| 1929 | sequence_function_to_b(Function, BPOS, TParams, TCall), | |
| 1930 | !. | |
| 1931 | % util/boolean | |
| 1932 | translate_function_call(Name, Params, _Type, BPOS, Result) :- | |
| 1933 | maplist(translate_e_p, Params, TParams), | |
| 1934 | alloy_to_b_boolean_utility_function(Name, TParams, BPOS, Result). | |
| 1935 | % util/relation | |
| 1936 | translate_function_call(Name, Params, _Type, BPOS, Result) :- | |
| 1937 | maplist(translate_e_p, Params, TParams), | |
| 1938 | check_position(BPOS,alloy_to_b_relational_utility_function), | |
| 1939 | alloy_to_b_relational_utility_function(Name, TParams, BPOS, Result). | |
| 1940 | % util/integer with no direct counterparts in B | |
| 1941 | translate_function_call(Name, Params, _Type, BPOS, Result) :- | |
| 1942 | is_util_integer_natural_func(Name, UtilType, AlloyOp), | |
| 1943 | UtilType == integer, | |
| 1944 | maplist(translate_e_p_integer, Params, TParams), | |
| 1945 | alloy_to_b_integer_utility_function(AlloyOp, BPOS, TParams, Result). | |
| 1946 | % util/natural with no direct counterparts in B | |
| 1947 | translate_function_call(Name, Params, _Type, BPOS, Result) :- | |
| 1948 | is_util_integer_natural_func(Name, UtilType, AlloyOp), | |
| 1949 | UtilType == natural, | |
| 1950 | maplist(translate_e_p_integer, Params, TParams), | |
| 1951 | alloy_to_b_natural_utility_function(AlloyOp, BPOS, TParams, Result), | |
| 1952 | !. | |
| 1953 | % util/integer and util/natural with direct counterparts in B | |
| 1954 | translate_function_call(Name, Params, _Type, BPOS, Result) :- | |
| 1955 | length(Params, Arity), | |
| 1956 | alloy_to_b_integer_natural_utility_func(Name, Arity, BOp, ArgType, ReturnType), | |
| 1957 | !, % functions like plus, minus, mul, ... with integer arguments and result | |
| 1958 | ( ArgType = integer -> | |
| 1959 | maplist(translate_e_p_integer, Params, TParams) | |
| 1960 | ; maplist(translate_e_p, Params, TParams) | |
| 1961 | ), | |
| 1962 | ( ReturnType = integer -> | |
| 1963 | Result = set_extension(BPOS,[TCall]) % we add set_extension wrapper | |
| 1964 | ; Result = TCall | |
| 1965 | ), | |
| 1966 | TCall =.. [BOp,BPOS|TParams]. | |
| 1967 | % util/ordering | |
| 1968 | translate_function_call(FunName, Params, type([SignatureName|_],_), BPOS, TCall) :- | |
| 1969 | translate_e_p(SignatureName, TSignatureName), | |
| 1970 | get_clean_ordering_fun_name(FunName, CleanOrdFunName), | |
| 1971 | translate_ordering_function(CleanOrdFunName, Params, SignatureName, TSignatureName, BPOS, TCall). | |
| 1972 | % definition call for calls to user defined Alloy predicates and functions | |
| 1973 | translate_function_call(Name, Params, _, BPOS, TCall) :- | |
| 1974 | % predicate and function call | |
| 1975 | maplist(translate_e_p, Params, TParams), | |
| 1976 | ( (definition_without_param(Name), TParams = [TParam]) | |
| 1977 | -> TCall = image(BPOS,definition(BPOS,Name,[]),TParam) | |
| 1978 | ; maplist(strip_singleton_set_from_this, TParams, TTParams), % identifier 'this' is added for fields which is already wrapped in a set extension | |
| 1979 | TCall = definition(BPOS,Name,TTParams) | |
| 1980 | ). | |
| 1981 | ||
| 1982 | % first: IF S_ord /= {} THEN {min(S_ord)} ELSE {} | |
| 1983 | 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))) :- | |
| 1984 | !. | |
| 1985 | % last: IF S_ord /= {} THEN {max(S_ord)} ELSE {} | |
| 1986 | 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))) :- | |
| 1987 | !. | |
| 1988 | % min[p]: IF p /= {} THEN {min(p)} ELSE {} | |
| 1989 | % max[p]: IF p /= {} THEN {min(p)} ELSE {} | |
| 1990 | translate_ordering_function(FunName, [Param], _, _, BPOS, TCall) :- | |
| 1991 | ( FunName == min | |
| 1992 | ; FunName == max | |
| 1993 | ), | |
| 1994 | !, | |
| 1995 | translate_e_p(Param, TParam), | |
| 1996 | InnerCall =.. [FunName,BPOS,TParam], | |
| 1997 | TCall = if_then_else(BPOS,not_equal(BPOS,TParam,empty_set(BPOS)),set_extension(BPOS,[InnerCall]),empty_set(BPOS)). | |
| 1998 | translate_ordering_function(FunName, [TParam], SignatureName, _, BPOS, TCall) :- | |
| 1999 | ( FunName == next | |
| 2000 | ; FunName == nexts | |
| 2001 | ; FunName == prev | |
| 2002 | ; FunName == prevs | |
| 2003 | ), | |
| 2004 | !, | |
| 2005 | get_ordering_definition_name(FunName, SignatureName, DefName), | |
| 2006 | translate_e_p(TParam, TTParam), | |
| 2007 | strip_singleton_set_from_this(TTParam, Param), | |
| 2008 | % The definition is something like this: next_House(s) == IF succ()[s] <: House THEN succ()[s] ELSE {} END | |
| 2009 | TCall = definition(BPOS,DefName,[Param]). | |
| 2010 | % larger[p1,p1]: IF p1 \/ p2 /= {} THEN {max(p1 \/ p2)} ELSE {} END | |
| 2011 | % smaller[p1,p2]: IF p1 \/ p2 /= {} THEN {min(p1 \/ p2)} ELSE {} END | |
| 2012 | translate_ordering_function(FunName, [P1,P2], _, _, BPOS, TCall) :- | |
| 2013 | ( FunName == larger | |
| 2014 | ; FunName == smaller | |
| 2015 | ), | |
| 2016 | !, | |
| 2017 | get_partial_b_functor_for_ordering(FunName, BFunctor), | |
| 2018 | translate_e_p(P1, TP1), | |
| 2019 | translate_e_p(P2, TP2), | |
| 2020 | ParamUnion = union(BPOS,TP1,TP2), | |
| 2021 | TInnerCall =.. [BFunctor,BPOS,ParamUnion], | |
| 2022 | InnerCall = set_extension(BPOS,[TInnerCall]), | |
| 2023 | TCall = if_then_else(BPOS,not_equal(BPOS,ParamUnion,empty_set(BPOS)),InnerCall,empty_set(BPOS)). | |
| 2024 | % lt[p1,p2]: (p1 = {}) or (p1 /= {} & p2 /= {} & p1 /= p2 & {min(p1 \/ p2)} = p1)) | |
| 2025 | % gt[p1,p2]: (p1 = {}) or (p1 /= {} & p2 /= {} & p1 /= p2 & {max(p1 \/ p2)} = p1)) | |
| 2026 | translate_ordering_function(FunName, [P1,P2], _, _, BPOS, TCall) :- | |
| 2027 | ( FunName == lt | |
| 2028 | ; FunName == gt | |
| 2029 | ), | |
| 2030 | !, | |
| 2031 | get_partial_b_functor_for_ordering(FunName, BFunctor), | |
| 2032 | translate_e_p(P1, TP1), | |
| 2033 | translate_e_p(P2, TP2), | |
| 2034 | TInnerCall =.. [BFunctor,BPOS,union(BPOS,TP1,TP2)], | |
| 2035 | InnerCall = set_extension(BPOS,[TInnerCall]), | |
| 2036 | LHS = equal(BPOS,TP1,empty_set(BPOS)), | |
| 2037 | RHS = conjunct(BPOS,conjunct(BPOS,conjunct(BPOS,not_equal(BPOS,TP1,empty_set(BPOS)), | |
| 2038 | not_equal(BPOS,TP2,empty_set(BPOS))), | |
| 2039 | not_equal(BPOS,TP1,TP2)), | |
| 2040 | equal(BPOS,InnerCall,TP1)), | |
| 2041 | TCall = disjunct(BPOS,LHS,RHS). | |
| 2042 | % lte[p1,p2]: (p1 = {}) or (p1 /= {} & p2 /= {} & {min(p1 \/ p2)} = p1) | |
| 2043 | % gte[p1,p2]: (p1 = {}) or (p1 /= {} & p2 /= {} & {max(p1 \/ p2)} = p1) | |
| 2044 | translate_ordering_function(FunName, [P1,P2], _, _, BPOS, TCall) :- | |
| 2045 | ( FunName == lte | |
| 2046 | ; FunName == gte | |
| 2047 | ), | |
| 2048 | !, | |
| 2049 | get_partial_b_functor_for_ordering(FunName, BFunctor), | |
| 2050 | translate_e_p(P1, TP1), | |
| 2051 | translate_e_p(P2, TP2), | |
| 2052 | TInnerCall =.. [BFunctor,BPOS,union(BPOS,TP1,TP2)], | |
| 2053 | InnerCall = set_extension(BPOS,[TInnerCall]), | |
| 2054 | LHS = equal(BPOS,TP1,empty_set(BPOS)), | |
| 2055 | RHS = conjunct(BPOS,conjunct(BPOS,not_equal(BPOS,TP1,empty_set(BPOS)), | |
| 2056 | not_equal(BPOS,TP2,empty_set(BPOS))), | |
| 2057 | equal(BPOS,InnerCall,TP1)), | |
| 2058 | TCall = disjunct(BPOS,LHS,RHS). | |
| 2059 | translate_ordering_function(FunName, [], SignatureName, _, BPOS, Res) :- | |
| 2060 | % ordering without argument used in a unary operator, e.g., 'some t : Trace | all s : t.^next | s.state = Off' | |
| 2061 | % as used in reset_flip_flop_with_enable.als | |
| 2062 | % for binary operators, we can inline joins as is done in annotate_undefined_ordering_definition_call/3 | |
| 2063 | ( FunName == next | |
| 2064 | ; FunName == nexts | |
| 2065 | ; FunName == prev | |
| 2066 | ; FunName == prevs | |
| 2067 | ), | |
| 2068 | !, | |
| 2069 | get_ordering_definition_name(FunName, SignatureName, DefName), | |
| 2070 | % e.g., generate %x.(x:House|MU(next_House({x}))) | |
| 2071 | TCall = mu(BPOS,definition(BPOS,DefName,[TParam])), | |
| 2072 | TId = identifier(BPOS,'_o_0'), | |
| 2073 | TParam = set_extension(BPOS,[TId]), | |
| 2074 | Member = member(BPOS,TId,identifier(BPOS,SignatureName)), | |
| 2075 | Res = lambda(BPOS,[TId],Member,TCall). | |
| 2076 | translate_ordering_function(FunName, Params, SignatureName, _Type, BPOS, empty_set(BPOS)) :- | |
| 2077 | length(Params,Arity), | |
| 2078 | ajoin(['Cannot translate ordering function for ',SignatureName,':'],Msg), | |
| 2079 | add_error(translate_ordering_function, Msg, FunName/Arity, BPOS). | |
| 2080 | ||
| 2081 | get_partial_b_functor_for_ordering(larger, max). | |
| 2082 | get_partial_b_functor_for_ordering(smaller, min). | |
| 2083 | get_partial_b_functor_for_ordering(lt, min). | |
| 2084 | get_partial_b_functor_for_ordering(lte, min). | |
| 2085 | get_partial_b_functor_for_ordering(gt, max). | |
| 2086 | get_partial_b_functor_for_ordering(gte, max). | |
| 2087 | ||
| 2088 | strip_singleton_set(set_extension(_,[identifier(Pos,Name)]), identifier(Pos,Name)) :- | |
| 2089 | !. | |
| 2090 | strip_singleton_set(A, A). | |
| 2091 | ||
| 2092 | strip_singleton_set_from_this(set_extension(_,[identifier(Pos,this)]), identifier(Pos,this)) :- | |
| 2093 | !. | |
| 2094 | strip_singleton_set_from_this(A, A). | |
| 2095 | ||
| 2096 | translate_cartesian(TPos, Arg1, Arg2, Res) :- | |
| 2097 | translate_e_p(Arg1, TArg1), | |
| 2098 | translate_cartesian2(TPos, TArg1, Arg2, Res). | |
| 2099 | ||
| 2100 | translate_cartesian2(TPos, TArg1, Arg2, Res) :- | |
| 2101 | translate_e_p(Arg2, TArg2), | |
| 2102 | translate_cartesian3(TPos, TArg1, Arg2, TArg2, Res). | |
| 2103 | % P -> Q --> P*Q | |
| 2104 | translate_cartesian3(TPos, TArg1, Arg2, TArg2, cartesian_product(TPos,TArg1,TArg2)) :- | |
| 2105 | is_unary_relation(Arg2), | |
| 2106 | !. | |
| 2107 | % P -> Q --> {c0, c1,...,ck | c0:P & (c1,...,ck):Q} | |
| 2108 | translate_cartesian3(TPos, TArg1, Arg2, TArg2, comprehension_set(TPos,[ID0|IDs2],conjunct(TPos,Mem1,Mem2))) :- | |
| 2109 | get_type_and_arity_from_alloy_term(Arg2, _Type, Arity), | |
| 2110 | gen_ids_and_couple(Arity, IDs2, Couple2), | |
| 2111 | gen_identifier(0, "_c_", ID0), | |
| 2112 | check_position(TPos,translate_cartesian3), | |
| 2113 | Mem1 = member(TPos,ID0,TArg1), | |
| 2114 | Mem2 = member(TPos,Couple2,TArg2). | |
| 2115 | ||
| 2116 | gen_ids_and_couple(Arity, [ID1|IDListRest], NestedCouple) :- | |
| 2117 | Arity > 0, | |
| 2118 | gen_identifier(1, "_c_", ID1), | |
| 2119 | gen_ids_and_couple(2, Arity, IDListRest, ID1, NestedCouple). | |
| 2120 | ||
| 2121 | gen_ids_and_couple(Nr, Arity, L, Acc, Res) :- | |
| 2122 | Nr > Arity, | |
| 2123 | !, | |
| 2124 | L = [], | |
| 2125 | Res = Acc. | |
| 2126 | gen_ids_and_couple(Nr, Arity, [IDN|T], Acc, Res) :- | |
| 2127 | gen_identifier(Nr, "_c_", IDN), | |
| 2128 | N1 is Nr+1, | |
| 2129 | gen_ids_and_couple(N1, Arity, T, couple(none,Acc,IDN), Res). | |
| 2130 | ||
| 2131 | gen_identifier(Nr, Prefix, identifier(none,ID)) :- | |
| 2132 | number_codes(Nr, NrC), | |
| 2133 | append(Prefix, NrC, AC), | |
| 2134 | atom_codes(ID, AC). | |
| 2135 | ||
| 2136 | is_ordering_definition_call(FunCall) :- | |
| 2137 | FunCall =.. [Functor,Name,_,_,_], | |
| 2138 | Functor == fun_call, | |
| 2139 | atom_concat('ordering\'', Rest, Name), | |
| 2140 | memberchk(Rest, [next,prev,nexts,prevs]). | |
| 2141 | ||
| 2142 | %% annotate_undefined_ordering_definition_call(+AlloyTerm, +AnnotateWith, -AnnotatedAlloyTerm). | |
| 2143 | % Top-level call is assumed to be a join. We join "undefined" ordering definition calls in | |
| 2144 | % arguments of the top-level join with an Alloy term. | |
| 2145 | % For instance: | |
| 2146 | % 'this.(prev + next)', where it actually is 'this.prev + this.next' as used in einsteins_enum.als | |
| 2147 | annotate_undefined_ordering_definition_call(Atom, _, Out) :- | |
| 2148 | atom(Atom), | |
| 2149 | !, | |
| 2150 | Out = Atom. | |
| 2151 | annotate_undefined_ordering_definition_call(join(Arg1,Arg2,Type,POS), AnnotateWith, Annotated) :- | |
| 2152 | is_ordering_definition_call(Arg1), | |
| 2153 | !, | |
| 2154 | annotate_undefined_ordering_definition_call(Arg2, AnnotateWith, NArg2), | |
| 2155 | Annotated = join(Arg1,NArg2,Type,POS). | |
| 2156 | annotate_undefined_ordering_definition_call(join(Arg1,Arg2,Type,POS), AnnotateWith, Annotated) :- | |
| 2157 | is_ordering_definition_call(Arg2), | |
| 2158 | !, | |
| 2159 | annotate_undefined_ordering_definition_call(Arg1, AnnotateWith, NArg1), | |
| 2160 | Annotated = join(NArg1,Arg2,Type,POS). | |
| 2161 | annotate_undefined_ordering_definition_call(Binary, AnnotateWith, Annotated) :- | |
| 2162 | % TODO: nested join with different top-level ordering definition call here? | |
| 2163 | functor(Binary, BFun, 4), | |
| 2164 | !, | |
| 2165 | arg(1, Binary, Arg1), | |
| 2166 | arg(2, Binary, Arg2), | |
| 2167 | arg(3, Binary, Type), | |
| 2168 | arg(4, Binary, POS), | |
| 2169 | ( is_ordering_definition_call(Arg1) | |
| 2170 | -> get_alloy_position(Arg1, A1POS), | |
| 2171 | get_alloy_type(Arg1, Arg1Type), | |
| 2172 | NArg1 = join(AnnotateWith,Arg1,Arg1Type,A1POS) | |
| 2173 | ; annotate_undefined_ordering_definition_call(Arg1, AnnotateWith, NArg1) | |
| 2174 | ), | |
| 2175 | ( is_ordering_definition_call(Arg2) | |
| 2176 | -> get_alloy_position(Arg2, A2POS), | |
| 2177 | get_alloy_type(Arg2, Arg2Type), | |
| 2178 | NArg2 = join(AnnotateWith,Arg2,Arg2Type,A2POS) | |
| 2179 | ; annotate_undefined_ordering_definition_call(Arg2, AnnotateWith, NArg2) | |
| 2180 | ), | |
| 2181 | functor(Annotated, BFun, 4), | |
| 2182 | arg(1, Annotated, NArg1), | |
| 2183 | arg(2, Annotated, NArg2), | |
| 2184 | arg(3, Annotated, Type), | |
| 2185 | arg(4, Annotated, POS). | |
| 2186 | annotate_undefined_ordering_definition_call(AlloyTerm, _, AlloyTerm). | |
| 2187 | ||
| 2188 | atom_ends_with(Atom, EndsWith) :- | |
| 2189 | atom_concat(_, EndsWith, Atom). | |
| 2190 | ||
| 2191 | % ordering function calls like s.next.next are converted to fun_call | |
| 2192 | translate_join(_, Arg1, Arg2, TBinaryJoin) :- | |
| 2193 | Arg2 = fun_call(Name,[],Type,A2Pos), | |
| 2194 | \+ atom_prefix('integer', Name), | |
| 2195 | \+ atom_ends_with(Name, 'first'), % one can use just first or last without a join while the actual Signature is inferred by its type | |
| 2196 | \+ atom_ends_with(Name, 'last'), % e.g., see ring_election1.als 'no elected.first' where elected is an ordered signature field of sig P | |
| 2197 | % 'no elected.first' is thus equivalent to 'no elected.(P.first)' | |
| 2198 | translate_e_p(fun_call(Name,[Arg1],Type,A2Pos), TBinaryJoin). | |
| 2199 | % Translation of the dot join operator has several special cases depending on the arity of the arguments. | |
| 2200 | translate_join(TPos, Arg1, Arg2, TBinaryJoin) :- | |
| 2201 | translate_e_p(Arg1, TArg1), | |
| 2202 | translate_e_p(Arg2, TArg2), | |
| 2203 | translate_join_aux(TPos, Arg1, Arg2, TArg1, TArg2, TBinaryJoin). | |
| 2204 | ||
| 2205 | % Note: N-ary relation are encoded in B as follows: | |
| 2206 | % { (e1 |-> (e2 |-> (e3 |-> ...))) ,... }, for example: | |
| 2207 | % {(tracy|->(spanish|->french)),(carol|->(spanish|->french)), ...} | |
| 2208 | % univ.P --> ran(P) % this does NOT work for ternary,... relations | |
| 2209 | translate_join_aux(TPos, Arg1, Arg2, _TArg1, TArg2, range(TPos,TArg2)) :- | |
| 2210 | is_univ(Arg1), | |
| 2211 | is_binary_relation(Arg2), | |
| 2212 | !. | |
| 2213 | % P.univ --> dom(P) % this works for ternary,... relations | |
| 2214 | translate_join_aux(TPos, _Arg1, Arg2, TArg1, _TArg2, domain(TPos,TArg1)) :- | |
| 2215 | is_univ(Arg2), | |
| 2216 | !. | |
| 2217 | % {el}.R --> {R(el)} | |
| 2218 | translate_join_aux(TPos, Arg1, Arg2, TArg1, TArg2, set_extension(TPos,[function(TPos,TArg2,[TTArg1])])) :- | |
| 2219 | get_type_and_arity_from_alloy_term(Arg1, Type1, Arity), | |
| 2220 | Arity = 1, % is_unary_relation(Arg1), | |
| 2221 | is_binary_relation(Arg2), % TO DO: Arg2 can probably be n-ary? | |
| 2222 | is_total_function(TArg2, Type1), | |
| 2223 | can_remove_singleton_set(TArg1, TTArg1), | |
| 2224 | !. | |
| 2225 | % unary.R --> R[unary] | |
| 2226 | translate_join_aux(TPos, Arg1, Arg2, TArg1, TArg2, Join) :- % Unary.Arg2 --> Arg2[Unary] | |
| 2227 | is_unary_relation(Arg1), | |
| 2228 | is_binary_relation(Arg2), | |
| 2229 | !, | |
| 2230 | Join = image(TPos,TArg2,TArg1). | |
| 2231 | % binary.unary | |
| 2232 | % Next RULE is broken, can lead to Type errors and test is wrong: | |
| 2233 | % translate_join_aux(Pos,Arg1,Arg2,TArg1,TArg2,function(Pos,reverse(Pos,TArg1),[TTArg2])) :- | |
| 2234 | % % function call if lhs is a total function and rhs a unary relation | |
| 2235 | % is_binary_relation(Arg1), | |
| 2236 | % is_unary_relation(Arg2), | |
| 2237 | % is_total_function(TArg1) , ! , % TEST SHOULD BE SURJECTIVE and INJECTIVE !! | |
| 2238 | % remove_singleton_set(TArg2,TTArg2). | |
| 2239 | % Arg1.Unary --> Arg1~[Unary] | |
| 2240 | translate_join_aux(TPos, _Arg1, Arg2, TArg1, TArg2, image(TPos,reverse(TPos,TArg1),TArg2)) :- | |
| 2241 | is_unary_relation(Arg2), | |
| 2242 | !. | |
| 2243 | % binary.binary: Arg1.Arg2 --> (Arg1 ; Arg2) | |
| 2244 | translate_join_aux(TPos, Arg1, Arg2, TArg1, TArg2, composition(TPos,TArg1,TArg2)) :- | |
| 2245 | is_binary_relation(Arg1), | |
| 2246 | is_binary_relation(Arg2), | |
| 2247 | !. | |
| 2248 | translate_join_aux(TPos, Arg1, Arg2, TArg1, TArg2, comprehension_set(TPos,IDS,Body)) :- | |
| 2249 | Body = conjunct(TPos,TypingPred,exists(TPos,[JoinID],conjunct(TPos,JoinTypingPred,conjunct(TPos,Mem1,Mem2)))), | |
| 2250 | get_type_and_arity_from_alloy_term(Arg2, [JoinIDType|RTypes], Arity), % first type refers to outter variable | |
| 2251 | gen_ids_and_couple(Arity, IDs2, Couple2), | |
| 2252 | IDs2 = [JoinID|Rest2], | |
| 2253 | get_typing_pred_for_ids(TPos, RTypes, Rest2, TypingPred), | |
| 2254 | get_typing_pred_for_ids(TPos, [JoinIDType], [JoinID], JoinTypingPred), | |
| 2255 | ( is_univ(Arg1) -> | |
| 2256 | Mem1 = truth(TPos), | |
| 2257 | IDS = Rest2 | |
| 2258 | ; is_unary_relation(Arg1) -> | |
| 2259 | %strip_singleton_set_from_this(TArg1, TTArg1), | |
| 2260 | Mem1 = member(TPos,JoinID,TArg1), | |
| 2261 | IDS = Rest2 | |
| 2262 | ; gen_identifier(0, "_c_", ID0), | |
| 2263 | IDS = [ID0|Rest2], | |
| 2264 | Mem1 = member(TPos,couple(TPos,ID0,JoinID),TArg1) | |
| 2265 | ), | |
| 2266 | check_position(TPos,translate_join_aux), | |
| 2267 | Mem2 = member(TPos,Couple2,TArg2). | |
| 2268 | translate_join_aux(Pos, Arg1, Arg2, _TArg1, _TArg2, empty_set(Pos)) :- | |
| 2269 | format('~nJoin not supported this way:~nLeft: ~w~nRight: ~w~n', [Arg1,Arg2]), | |
| 2270 | add_error(load_alloy_model, 'Cannot translate this type of join yet', [Arg1,Arg2], Pos). | |
| 2271 | ||
| 2272 | % This predicate relies on the order of elements in 2. and 3. argument for typing. | |
| 2273 | % TO DO: improve | |
| 2274 | get_typing_pred_for_ids(Pos, [], [], truth(Pos)). | |
| 2275 | get_typing_pred_for_ids(Pos, [Type|TT], [ID|IT], TypingPred) :- | |
| 2276 | translate_e_p(Type, TType), | |
| 2277 | get_typing_pred_for_ids_acc(Pos, TT, IT, member(Pos,ID,TType), TypingPred). | |
| 2278 | ||
| 2279 | get_typing_pred_for_ids_acc(_, [], [], Acc, Acc). | |
| 2280 | get_typing_pred_for_ids_acc(Pos, [Type|TT], [ID|IT], Acc, TypingPred) :- | |
| 2281 | translate_e_p(Type, TType), | |
| 2282 | get_typing_pred_for_ids_acc(Pos, TT, IT, conjunct(Pos,Acc,member(Pos,ID,TType)), TypingPred). | |
| 2283 | ||
| 2284 | % translate Alloy position to B position | |
| 2285 | translate_pos(Var,Res) :- \+ ground(Var),!, | |
| 2286 | add_internal_error('Translating non-ground Alloy position to none:',translate_pos(Var,Res)), | |
| 2287 | Res=none. | |
| 2288 | translate_pos(pos(Col,Row), Res) :- nonvar(Col), nonvar(Row), | |
| 2289 | !, | |
| 2290 | row_col_to_position(Row,Col,Res). | |
| 2291 | translate_pos(_, none). | |
| 2292 | ||
| 2293 | %get_position(Term, BPos) :- | |
| 2294 | % get_alloy_position(Term, APos), | |
| 2295 | % !, | |
| 2296 | % translate_pos(APos, BPos). | |
| 2297 | %get_position(_, none). | |
| 2298 | ||
| 2299 | get_alloy_type(Term, AType) :- | |
| 2300 | functor(Term, _, Arity), | |
| 2301 | Arity > 0, | |
| 2302 | Arity1 is Arity - 1, | |
| 2303 | arg(Arity1, Term, AType). | |
| 2304 | ||
| 2305 | get_alloy_position(Term, APos) :- | |
| 2306 | functor(Term, _, Arity), | |
| 2307 | Arity > 0, | |
| 2308 | arg(Arity, Term, APos). | |
| 2309 | ||
| 2310 | get_b_position(UntypedBAst, BPOS) :- | |
| 2311 | functor(UntypedBAst, _, Arity), | |
| 2312 | Arity > 0, | |
| 2313 | arg(1, UntypedBAst, BPOS). | |
| 2314 | ||
| 2315 | check_position(Var,PP) :- var(Var),!,add_internal_error('Variable position at: ',PP),Var=none. | |
| 2316 | check_position(P,_) :- is_valid_position(P),!. | |
| 2317 | check_position(T,PP) :- add_warning(check_position,'Unknown position at: ',PP:T). | |
| 2318 | ||
| 2319 | translate_quantified_e(Pos, no, TArg, equal(Pos,TArg,empty_set(none))). | |
| 2320 | translate_quantified_e(Pos, AlloyKw, TArg, equal(Pos,card(none,TArg),integer(none,1))) :- | |
| 2321 | % naming possibly differs having the same semantics | |
| 2322 | AlloyKw = one; AlloyKw = oneof. | |
| 2323 | translate_quantified_e(Pos, AlloyKw, TArg, greater(Pos,card(none,TArg),integer(none,0))) :- | |
| 2324 | AlloyKw = some; AlloyKw = someof. | |
| 2325 | translate_quantified_e(Pos, AlloyKw, TArg, less_equal(Pos,card(none,TArg),integer(none,1))) :- | |
| 2326 | AlloyKw = lone; AlloyKw = loneof. | |
| 2327 | translate_quantified_e(_, exactlyof, TArg, TArg). | |
| 2328 | ||
| 2329 | % Join a list of types using cartesian_product like ((A*B)*C) for types [A,B,C]. | |
| 2330 | create_cartesian_type([ID], TID) :- | |
| 2331 | !, | |
| 2332 | translate_unary_e_p(ID, TID). | |
| 2333 | create_cartesian_type([ID1,ID2], cartesian_product(none,TID1,TID2)) :- | |
| 2334 | !, | |
| 2335 | translate_unary_e_p(ID1, TID1), | |
| 2336 | translate_unary_e_p(ID2, TID2). | |
| 2337 | create_cartesian_type([ID1,ID2|T], cartesian_product(none,cartesian_product(none,TID1,TID2),NT)) :- | |
| 2338 | translate_unary_e_p(ID1, TID1), | |
| 2339 | translate_unary_e_p(ID2, TID2), | |
| 2340 | create_cartesian_type(T, NT). | |
| 2341 | ||
| 2342 | % Field declarations have several special cases depending on the keywords set, one, some, lone or seq. | |
| 2343 | % We are inside Signature TSignatureName sig NAME { field : DeclTerm } | |
| 2344 | translate_field_decl(BPOS, SignatureName, TSignatureName, DeclTerm, FieldID, TFieldID, TFieldPred) :- | |
| 2345 | % DeclTerm =.. [_,SetID|_], | |
| 2346 | replace_this_in_signature_field(DeclTerm, NewDeclTerm), | |
| 2347 | debug_format(19, 'Translating Field ~w inside signature ~w,~n Term=~w,~n~n', [FieldID,SignatureName,NewDeclTerm]), | |
| 2348 | ( translate_special_field_multiplicity_binary_e_p(NewDeclTerm, TFUNC) | |
| 2349 | -> | |
| 2350 | % we could do: translate_cartesian2(BPOS,TSignatureName,NewDeclTerm,Cart), TFieldPred = subset(BPOS,TFieldID,Cart), and add predicate | |
| 2351 | % TO DO: better treatment, also detect nested special multiplicity annotations inside NewDeclTerm | |
| 2352 | % generate forall x:SIG => x.field : TFUNC | |
| 2353 | ID = identifier(BPOS,'_x_'), | |
| 2354 | AID = identifier('_x_',type([SignatureName],1),none), | |
| 2355 | ( singleton_set('_x_') -> | |
| 2356 | true | |
| 2357 | ; assert_singleton_set('_x_') | |
| 2358 | ), | |
| 2359 | translate_e_p(AID, TAID), % will add set-extension wrapper | |
| 2360 | LHS = member(BPOS,ID,TSignatureName), | |
| 2361 | RHS = member(BPOS,TJoin,TFUNC), | |
| 2362 | TFieldPred = conjunct(BPOS,FieldTyping,forall(BPOS,[ID],implication(none,LHS,RHS))), | |
| 2363 | translate_join_aux(BPOS, AID, FieldID, TAID, TFieldID, TJoin), | |
| 2364 | get_type_and_arity_from_alloy_term(FieldID, TypeList, _), | |
| 2365 | create_cartesian_type(TypeList, CartesianType), | |
| 2366 | FieldTyping = member(BPOS,TFieldID,pow_subset(BPOS,CartesianType)) | |
| 2367 | ; translate_sig_field_rhs(FieldID, NewDeclTerm, BPOS, TSignatureName, TFieldID, FieldTypeExpr) | |
| 2368 | -> | |
| 2369 | add_constraint_for_someof_field(NewDeclTerm, member(BPOS,TFieldID,FieldTypeExpr), TSignatureName, TTFieldPred), | |
| 2370 | add_constraint_for_seq_field(NewDeclTerm, TSignatureName, TTFieldPred, TFieldID, TFieldPred) | |
| 2371 | ; add_error(alloy2b, 'Field declaration not implemented:', NewDeclTerm, BPOS), | |
| 2372 | TFieldPred = truth(none) | |
| 2373 | ). | |
| 2374 | ||
| 2375 | add_constraint_for_someof_field(someof(_,_,_), TempPred, TSignatureName, TPred) :- | |
| 2376 | !, | |
| 2377 | TempPred = member(BPOS,TFieldID,_), | |
| 2378 | TPred = conjunct(BPOS,equal(BPOS,domain(BPOS,TFieldID),TSignatureName),TempPred). | |
| 2379 | add_constraint_for_someof_field(_, Pred, _, Pred). | |
| 2380 | ||
| 2381 | add_constraint_for_seq_field('is_seq'(_,_,_), TSignatureName, TempPred, TFieldID, TPred) :- | |
| 2382 | !, | |
| 2383 | % !_s.(_s : TSignatureName => dom(TFieldID)[{_s}] = 0..card(dom(TFieldID)[{_s}])-1) | |
| 2384 | TPred = conjunct(BPOS,TempPred,forall([identifier(BPOS,'_s')], | |
| 2385 | implication(BPOS,member(identifier(BPOS,'_s'),TSignatureName), | |
| 2386 | equal(BPOS,image(BPOS,domain(BPOS,TFieldID),set_extension(BPOS,[identifier(BPOS,'_s')])), | |
| 2387 | interval(BPOS,integer(BPOS,0),minus(BPOS,card(BPOS,image(BPOS,domain(BPOS,TFieldID), | |
| 2388 | set_extension(BPOS,[identifier(BPOS,'_s')]))),integer(BPOS,1))))))). | |
| 2389 | add_constraint_for_seq_field(_, _, Pred, _, Pred). | |
| 2390 | ||
| 2391 | % sig SIG { field : set Set} --> field : SIG <-> Set | |
| 2392 | translate_sig_field_rhs(_, setof(Set,_,_), _, SIG, _, relations(none,SIG,TSet)) :- | |
| 2393 | translate_e_p(Set, TSet). | |
| 2394 | % sig SIG { field : one Set} --> field : SIG --> Set | |
| 2395 | translate_sig_field_rhs(_, oneof(Set,_,_), _, SIG, TFieldID, total_function(none,SIG,TSet)) :- | |
| 2396 | translate_e_p(Set, TSet), | |
| 2397 | assert_total_function(TFieldID, SIG). | |
| 2398 | % sig SIG { field : lone Set} --> field : SIG +-> Set | |
| 2399 | translate_sig_field_rhs(_, loneof(Set,_,_), _, SIG, _, partial_function(none,SIG,TSet)) :- | |
| 2400 | translate_e_p(Set, TSet). | |
| 2401 | % sig SIG { field : some Set} --> field : SIG +-> Set | |
| 2402 | translate_sig_field_rhs(_, someof(Set,_,_), _, SIG, _, relations(none,SIG,TSet)) :- | |
| 2403 | translate_e_p(Set, TSet). | |
| 2404 | % sig SIG { field : seq Set} --> field : (SIG * Integer) +-> Set | |
| 2405 | 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)) :- | |
| 2406 | maxseq(MaxSeq), | |
| 2407 | MaxSeq1 is MaxSeq - 1, | |
| 2408 | FieldID = identifier(Name,Type,_), | |
| 2409 | prepend_identifier_of_module_import(Name, Type, NName), | |
| 2410 | assertz(is_seq(NName)), | |
| 2411 | translate_e_p(Set, TSet). | |
| 2412 | % sig SIG { field : FieldTerm} --> field : POW(SIG * FieldTerm) | |
| 2413 | translate_sig_field_rhs(_, FieldTerm, Pos, SIG, _, pow_subset(none,Cart)) :- | |
| 2414 | % TO DO: check whether lone, one, ... can appear inside FieldTerm | |
| 2415 | translate_cartesian2(Pos, SIG, FieldTerm, Cart). | |
| 2416 | ||
| 2417 | replace_this_in_signature_field(identifier('this',type([SignatureName],1),Pos), Res) :- | |
| 2418 | !, | |
| 2419 | Res = identifier(SignatureName,type([SignatureName],1),Pos). | |
| 2420 | replace_this_in_signature_field(DeclTerm, NewDeclTerm) :- | |
| 2421 | DeclTerm =.. [Functor,Arg1,Type,Pos], | |
| 2422 | !, | |
| 2423 | replace_this_in_signature_field(Arg1, NArg1), | |
| 2424 | NewDeclTerm =.. [Functor,NArg1,Type,Pos]. | |
| 2425 | replace_this_in_signature_field(DeclTerm, NewDeclTerm) :- | |
| 2426 | DeclTerm =.. [Functor,Arg1,Arg2,Type,Pos], | |
| 2427 | !, | |
| 2428 | replace_this_in_signature_field(Arg1, NArg1), | |
| 2429 | replace_this_in_signature_field(Arg2, NArg2), | |
| 2430 | NewDeclTerm =.. [Functor,NArg1,NArg2,Type,Pos]. | |
| 2431 | replace_this_in_signature_field(DeclTerm, DeclTerm). | |
| 2432 | ||
| 2433 | % Translate TFieldID: Declaration | |
| 2434 | fun_or_pred_decl_special_cases(setof(Expr,_,_), TFieldID, Pos, subset(Pos,TFieldID,TExpr), set) :- | |
| 2435 | translate_e_p(Expr, TExpr). | |
| 2436 | fun_or_pred_decl_special_cases(oneof(Expr,_,_), TFieldID, Pos, subset(Pos,TFieldID,TExpr), singleton) :- % Default | |
| 2437 | translate_e_p(Expr, TExpr). | |
| 2438 | fun_or_pred_decl_special_cases(loneof(Expr,_,_), TFieldID, Pos, conjunct(Pos,subset(Pos,TFieldID,TExpr),ExtraPred), set) :- | |
| 2439 | % x : lone S -> x <: S & card(x) <= 1 | |
| 2440 | ExtraPred = less_equal(Pos,card(Pos,TFieldID),integer(Pos,1)), | |
| 2441 | translate_e_p(Expr, TExpr). | |
| 2442 | fun_or_pred_decl_special_cases(someof(Expr,_,_), TFieldID, Pos, conjunct(Pos,subset(Pos,TFieldID,TExpr),ExtraPred), set) :- | |
| 2443 | % x : some S -> x <: S & x \= {} | |
| 2444 | ExtraPred = not_equal(Pos,TFieldID,empty_set(Pos)), | |
| 2445 | translate_e_p(Expr, TExpr). | |
| 2446 | fun_or_pred_decl_special_cases(Expr, TFieldID, Pos, Translation, IsSingleton) :- | |
| 2447 | % treat identifier, cartesian, union, ... use translate of TFieldID in Expr | |
| 2448 | translate_binary_in(TFieldID, Expr, Pos, Translation), | |
| 2449 | get_type_and_arity_from_alloy_term(Expr, _Type, Arity), | |
| 2450 | !, | |
| 2451 | ( Arity = 1 -> | |
| 2452 | IsSingleton = singleton | |
| 2453 | ; IsSingleton = set | |
| 2454 | ). | |
| 2455 | fun_or_pred_decl_special_cases(Term, _, Pos, falsity(Pos), set) :- | |
| 2456 | add_error(alloy2b, 'Field declaration for function or predicate not implemented:', Term, Pos). | |
| 2457 | ||
| 2458 | alloy_to_b_operator(Op, BOp) :- | |
| 2459 | alloy_to_b_unary_operator(Op, BOp), | |
| 2460 | !. | |
| 2461 | alloy_to_b_operator(Op, BOp) :- | |
| 2462 | alloy_to_b_binary_operator(Op, BOp), | |
| 2463 | !. | |
| 2464 | alloy_to_b_operator(Op, Op) :- | |
| 2465 | format('~n~nTRANSLATING ~w to B without modification!~n', [Op]). | |
| 2466 | ||
| 2467 | alloy_to_b_unary_operator(not, negation). | |
| 2468 | alloy_to_b_unary_operator(closure1, closure). | |
| 2469 | alloy_to_b_unary_operator(closure, reflexive_closure). | |
| 2470 | alloy_to_b_unary_operator(inverse, reverse). % works for binary relation only; indeed Alloy says: ~ can be used only with a binary relation. | |
| 2471 | ||
| 2472 | ||
| 2473 | alloy_to_b_binary_operator(in, subset). | |
| 2474 | alloy_to_b_binary_operator(not_in, not_subset). | |
| 2475 | alloy_to_b_binary_operator(plus, union). | |
| 2476 | alloy_to_b_binary_operator(or, disjunct). % actually treated as unary operator | |
| 2477 | alloy_to_b_binary_operator(and, conjunct). % actually treated as unary operator | |
| 2478 | alloy_to_b_binary_operator(minus, set_subtraction). | |
| 2479 | % alloy_to_b_binary_operator(cartesian,cartesian_product). % only works for X->UNARY ! | |
| 2480 | alloy_to_b_binary_operator(function, expression_definition). | |
| 2481 | alloy_to_b_binary_operator(predicate, predicate_definition). | |
| 2482 | alloy_to_b_binary_operator(not_equal, not_equal). | |
| 2483 | alloy_to_b_binary_operator(dom_restr, domain_restriction). % not ok for ternary, set must be unary | |
| 2484 | alloy_to_b_binary_operator(ran_restr, range_restriction). % also ok for ternary, ... relations | |
| 2485 | alloy_to_b_binary_operator(equal, equal). | |
| 2486 | alloy_to_b_binary_operator(conjunct, conjunct). | |
| 2487 | alloy_to_b_binary_operator(intersection, intersection). | |
| 2488 | alloy_to_b_binary_operator(implication, implication). | |
| 2489 | alloy_to_b_binary_operator(iff, equivalence). | |
| 2490 | alloy_to_b_binary_operator(override, overwrite). % ++ | |
| 2491 | ||
| 2492 | is_cartesian_product_term(Term, Arg1, Arg2, POS) :- | |
| 2493 | functor(Term, Functor, 4), | |
| 2494 | is_cartesian_product(Functor), | |
| 2495 | arg(1, Term, Arg1), | |
| 2496 | arg(2, Term, Arg2), | |
| 2497 | arg(4, Term, POS). | |
| 2498 | is_cartesian_product(cartesian). | |
| 2499 | ||
| 2500 | ||
| 2501 | % predicates with integer arguments | |
| 2502 | alloy_to_b_integer_operator(less, less). | |
| 2503 | alloy_to_b_integer_operator(greater, greater). | |
| 2504 | alloy_to_b_integer_operator(less_equal, less_equal). | |
| 2505 | alloy_to_b_integer_operator(greater_equal, greater_equal). | |
| 2506 | ||
| 2507 | ||
| 2508 | %%% | |
| 2509 | % Accumulate the translated machine parts and signature names during the translation and build the machine AST afterwards. | |
| 2510 | % We may need the signature names later on if translating a global scope. | |
| 2511 | build_machine_ast(b_machine(ListOfMachineParts,_SignatureNames), machine(generated(none,AbstractMachine))) :- | |
| 2512 | % filter empty machine parts | |
| 2513 | findall(MachinePart, ( member(MachinePart, ListOfMachineParts), | |
| 2514 | arg(2,MachinePart,L), | |
| 2515 | L \== [] | |
| 2516 | ), NonEmptyMachineSections), | |
| 2517 | % properties need to be conjoined | |
| 2518 | ( select(properties(none,L), NonEmptyMachineSections, RestListOfUsedMachineParts) -> | |
| 2519 | true | |
| 2520 | ; L == [], | |
| 2521 | RestListOfUsedMachineParts = NonEmptyMachineSections | |
| 2522 | ), | |
| 2523 | join_predicates(conjunct, L, FlatL), | |
| 2524 | AbstractMachine = abstract_machine(none,machine(none), | |
| 2525 | machine_header(none,alloytranslation,[]), | |
| 2526 | [properties(none,FlatL)|RestListOfUsedMachineParts]), | |
| 2527 | !. | |
| 2528 | ||
| 2529 | empty_machine_acc(b_machine([sets(none,[]),constants(none,[]), | |
| 2530 | definitions(none,[]),properties(none,[]), | |
| 2531 | assertions(none,[]),operations(none,[])],[])). | |
| 2532 | ||
| 2533 | % extend a machine section with a give list of conjuncts | |
| 2534 | extend_machine_with_conjuncts(_Section, [], Acc, Res) :- | |
| 2535 | !, | |
| 2536 | Res = Acc. | |
| 2537 | extend_machine_with_conjuncts(Section, Conjuncts, MAcc1, MAcc2) :- | |
| 2538 | join_untyped_ast_nodes(conjunct, Conjuncts, TPred), | |
| 2539 | extend_machine_acc(Section, MAcc1, TPred, MAcc2). | |
| 2540 | ||
| 2541 | :- if(environ(prob_safe_mode,true)). | |
| 2542 | extend_machine_acc(F, _, New, _) :- \+ ground(New), | |
| 2543 | add_internal_error('Non-ground new formula:',extend_machine_acc(F, _, New, _)), | |
| 2544 | fail. | |
| 2545 | :- endif. | |
| 2546 | extend_machine_acc(signatures, b_machine(MachineParts,SignatureNames), New, | |
| 2547 | b_machine(MachineParts,NewSignatureNames)) :- | |
| 2548 | !, | |
| 2549 | append(SignatureNames, New, TSignatureNames), | |
| 2550 | remove_dups(TSignatureNames, NewSignatureNames). | |
| 2551 | extend_machine_acc(Functor, b_machine(MachineParts,SignatureNames), New, | |
| 2552 | b_machine([NewMachinePart|RestMachineParts],SignatureNames)) :- | |
| 2553 | MachinePart =.. [Functor,none,List], | |
| 2554 | select(MachinePart, MachineParts, RestMachineParts), | |
| 2555 | append(List, [New], NewList), % keeps order, but is inefficient! | |
| 2556 | NewMachinePart =.. [Functor,none,NewList], | |
| 2557 | !. | |
| 2558 | extend_machine_acc(Functor, _, _, _) :- | |
| 2559 | add_internal_error('Failed: ', extend_machine_acc(Functor,_,_,_)), | |
| 2560 | fail. | |
| 2561 | ||
| 2562 | get_signature_names_from_machine_acc(b_machine(_MachineParts,SignatureNames), SignatureNames). | |
| 2563 | ||
| 2564 | finalize_extending_signatures(MAcc, NewMAcc) :- | |
| 2565 | extending_signatures(List), | |
| 2566 | !, | |
| 2567 | finalize_extending_signatures_aux(MAcc, List, NewMAcc). | |
| 2568 | finalize_extending_signatures(MAcc, MAcc). | |
| 2569 | ||
| 2570 | finalize_extending_signatures_aux(MAcc, [], MAcc). | |
| 2571 | finalize_extending_signatures_aux(MAcc, [(Parent,SubSigs)|T], NewMAcc) :- | |
| 2572 | length(SubSigs, AmountOfSubSigs), | |
| 2573 | AmountOfSubSigs > 1, | |
| 2574 | !, | |
| 2575 | maplist(translate_sub_sig, SubSigs, TSubSigs), | |
| 2576 | translate_e_p(Parent, TParent), | |
| 2577 | extend_machine_acc(properties, MAcc, partition(none,TParent,TSubSigs), MAcc2), | |
| 2578 | % equivalent to | |
| 2579 | % parent = sub1 \/ sub2 \/ ... \/ subN & sub1 /\ sub2 = {} & ... | |
| 2580 | findall(OneSub, member(OneSub/one, SubSigs), OneSubSigs), | |
| 2581 | length(OneSubSigs, AmountOneSubSigs), | |
| 2582 | ( AmountOneSubSigs = AmountOfSubSigs % we basically have an enumerated set with only singleton elements | |
| 2583 | -> | |
| 2584 | extend_machine_acc(properties, MAcc2, equal(none,card(none,TParent),integer(none,AmountOneSubSigs)), MAcc3) | |
| 2585 | ; extend_machine_acc(properties, MAcc2, greater_equal(none,card(none,TParent),integer(none,AmountOneSubSigs)), MAcc3) | |
| 2586 | ), | |
| 2587 | finalize_extending_signatures_aux(MAcc3, T, NewMAcc). | |
| 2588 | finalize_extending_signatures_aux(MAcc, [_|T], NewMAcc) :- | |
| 2589 | finalize_extending_signatures_aux(MAcc, T, NewMAcc). | |
| 2590 | %%% | |
| 2591 | translate_sub_sig(Name/_One, B) :- | |
| 2592 | translate_e_p(Name, B). | |
| 2593 | ||
| 2594 | assert_extending_signature(Name, Parent, One) :- | |
| 2595 | ( is_sub_signature_of(Name, Parent, One) -> | |
| 2596 | true | |
| 2597 | ; debug_format(19, '~w is sub signature of ~w (~w)~n', [Name,Parent,One]), | |
| 2598 | assertz(is_sub_signature_of(Name, Parent, One)) | |
| 2599 | ), | |
| 2600 | extending_signatures(List), | |
| 2601 | select((Parent,SubSigs), List, Rest), | |
| 2602 | !, | |
| 2603 | ( \+ memberchk(Name/One, SubSigs) | |
| 2604 | -> | |
| 2605 | retractall(extending_signatures(_)), | |
| 2606 | asserta(extending_signatures([(Parent,[Name/One|SubSigs])|Rest])) | |
| 2607 | ; true | |
| 2608 | ). | |
| 2609 | assert_extending_signature(Name, Parent, One) :- | |
| 2610 | retract(extending_signatures(List)), | |
| 2611 | !, | |
| 2612 | asserta(extending_signatures([(Parent,[Name/One])|List])). | |
| 2613 | assert_extending_signature(Name, Parent, One) :- | |
| 2614 | asserta(extending_signatures([(Parent,[Name/One])])). | |
| 2615 | ||
| 2616 | assert_enumerated_set(Options, Name) :- | |
| 2617 | % singleton top-level signatures are defined as an enumerated set like S = {_S} | |
| 2618 | member(one, Options), | |
| 2619 | % but extending singleton signatures are defined as constants and singleton subsets of their parent type | |
| 2620 | \+ member(subset(_), Options), | |
| 2621 | \+ member(subsig(_), Options), | |
| 2622 | !, | |
| 2623 | asserta(enumerated_set(Name)). | |
| 2624 | assert_enumerated_set(_, _). | |
| 2625 | ||
| 2626 | assert_abstract_sig(Options, Name) :- | |
| 2627 | member(abstract, Options), | |
| 2628 | !, | |
| 2629 | asserta(abstract_sig(Name)). | |
| 2630 | assert_abstract_sig(_, _). | |
| 2631 | ||
| 2632 | assert_singleton_set(Options, Name) :- | |
| 2633 | member(one, Options), | |
| 2634 | !, | |
| 2635 | assert_singleton_set(Name). | |
| 2636 | assert_singleton_set(_, _). | |
| 2637 | ||
| 2638 | assert_singleton_set(Name) :- % debug_format(19,'Singleton set : ~w~n',[Name]),nl, | |
| 2639 | % \+ singleton_set(Name), | |
| 2640 | asserta(singleton_set(Name)), | |
| 2641 | !. | |
| 2642 | % assert_singleton_set(_). | |
| 2643 | retract_singleton_set(BPOS, Name) :- | |
| 2644 | ( retract(singleton_set(Name)) -> true | |
| 2645 | ; Name = alloy2b_none -> true % avoid messages when running tests | |
| 2646 | ; add_message(retract_singleton_set, 'WARNING: no singleton_set fact for: ', Name, BPOS) % can be ok for non-singleton ids | |
| 2647 | ). | |
| 2648 | % retractall(singleton_set(Name)). | |
| 2649 | retract_state :- | |
| 2650 | % don't retract model_path here | |
| 2651 | retractall(fact(_)), | |
| 2652 | retractall(assertion(_)), | |
| 2653 | retractall(definition_without_param(_)), | |
| 2654 | retractall(skipped_command(_,_)), | |
| 2655 | retractall(translated_command(_,_)), | |
| 2656 | retractall(abstract_sig(_)), | |
| 2657 | retractall(sig_field_id(_, _)), | |
| 2658 | retractall(artificial_parent_type(_, _, _)), | |
| 2659 | retractall(current_module_in_scope(_)), | |
| 2660 | retractall(module_in_scope_but_root(_, _)), | |
| 2661 | retractall(enumerated_set(_)), | |
| 2662 | retractall(singleton_set(_)), | |
| 2663 | retractall(ordered_signature(_)), | |
| 2664 | retractall(total_function(_, _)), | |
| 2665 | retractall(extending_signatures(_)), | |
| 2666 | retractall(is_seq(_)), | |
| 2667 | retractall(maxseq(_)), | |
| 2668 | retractall(is_sub_signature_of(_, _, _)), | |
| 2669 | !. | |
| 2670 | ||
| 2671 | % an identifier which in B refers not to a set but an element of a set, representing a singleton set in Alloy | |
| 2672 | is_singleton_set_id(this). % this is always singleton (TO DO: check this ;-) | |
| 2673 | is_singleton_set_id(IDName) :- | |
| 2674 | singleton_set(IDName). | |
| 2675 | ||
| 2676 | assert_total_function(identifier(_,Name), SIG) :- | |
| 2677 | !, | |
| 2678 | assert_total_function(Name, SIG). | |
| 2679 | assert_total_function(Name, identifier(_,SIG)) :- | |
| 2680 | !, | |
| 2681 | assert_total_function(Name, SIG). | |
| 2682 | assert_total_function(Name, SIG) :- | |
| 2683 | debug_format(19, 'Total function ~w over ~w~n', [Name,SIG]), | |
| 2684 | asserta(total_function(Name, SIG)). | |
| 2685 | ||
| 2686 | is_total_function(predecessor(_), _). % translation of prev | |
| 2687 | is_total_function(successor(_), _). % translation of next | |
| 2688 | is_total_function(function(_,ID,_), ArgType) :- | |
| 2689 | !, | |
| 2690 | is_total_function(ID, ArgType). | |
| 2691 | is_total_function(identifier(_,Name), ArgType) :- | |
| 2692 | !, | |
| 2693 | is_total_function(Name, ArgType). | |
| 2694 | is_total_function(Name, [ArgType]) :- | |
| 2695 | total_function(Name, FunType), % TO DO: check if FunctionType is Superset of ArgType | |
| 2696 | ( strip_singleton_set(FunType, SFunType), | |
| 2697 | SFunType = identifier(_,ArgType) | |
| 2698 | -> true | |
| 2699 | ; ArgType = FunType -> true | |
| 2700 | ; is_sub_signature_of(ArgType, FunType, _) | |
| 2701 | ). | |
| 2702 | ||
| 2703 | assert_ordered_sig_name(Name) :- | |
| 2704 | asserta(ordered_signature(Name)). | |
| 2705 | ||
| 2706 | is_ordered_signature(IDName) :- | |
| 2707 | ordered_signature(IDName). | |
| 2708 | is_ordered_signature('ordering\''). | |
| 2709 | ||
| 2710 | is_univ(identifier('univ',_,_)). % universe | |
| 2711 | is_univ(identifier(_,'univ')). | |
| 2712 | ||
| 2713 | is_iden(iden(_)). | |
| 2714 | is_iden(event_b_identity(_)). | |
| 2715 | ||
| 2716 | is_unary_relation(AlloyTerm) :- | |
| 2717 | get_type_and_arity_from_alloy_term(AlloyTerm, _Type, Arity), | |
| 2718 | Arity == 1. | |
| 2719 | ||
| 2720 | is_binary_relation(AlloyTerm) :- | |
| 2721 | get_type_and_arity_from_alloy_term(AlloyTerm, _Type, Arity), | |
| 2722 | Arity == 2. | |
| 2723 | ||
| 2724 | can_remove_singleton_set(set_extension(_,[Element]), Element). | |
| 2725 | % remove_singleton_set(AST,AST). | |
| 2726 | get_type_and_arity_from_alloy_term(integer(_,_), Type, Arity) :- | |
| 2727 | !, | |
| 2728 | Type = integer, | |
| 2729 | Arity = 1. % will get translated to singleton set | |
| 2730 | get_type_and_arity_from_alloy_term(and(_,_), Type, Arity) :- | |
| 2731 | !, | |
| 2732 | Type = [untyped], | |
| 2733 | Arity = 0. % predicate | |
| 2734 | get_type_and_arity_from_alloy_term(or(_,_), Type, Arity) :- | |
| 2735 | !, | |
| 2736 | Type = [untyped], | |
| 2737 | Arity = 0. % predicate | |
| 2738 | get_type_and_arity_from_alloy_term(iden(_), Type, Arity) :- | |
| 2739 | !, | |
| 2740 | Type = univ, | |
| 2741 | Arity = 2. | |
| 2742 | get_type_and_arity_from_alloy_term(AlloyTerm, Type, NArity) :- | |
| 2743 | AlloyTerm =.. [_|Args], | |
| 2744 | member(type(Type,Arity), Args), | |
| 2745 | ( is_primitive_type(Type, NArity) | |
| 2746 | ; | |
| 2747 | ( length(Type, LType), | |
| 2748 | LType == Arity, | |
| 2749 | NArity = Arity | |
| 2750 | ) | |
| 2751 | ), | |
| 2752 | !. | |
| 2753 | get_type_and_arity_from_alloy_term(AlloyTerm, Type, Arity) :- | |
| 2754 | add_warning(alloy2b, 'Could not extract type and arity from Alloy term:', AlloyTerm), | |
| 2755 | Type = [untyped], | |
| 2756 | Arity = 0. % like predicate | |
| 2757 | ||
| 2758 | % TO DO: maybe there are more primitive types? | |
| 2759 | % primitive types have arity zero in Alloy for some reason | |
| 2760 | is_primitive_type(['PrimitiveBoolean'], 1). | |
| 2761 | ||
| 2762 | % atom_or_identifier_term(ID,ID) :- atom(ID). | |
| 2763 | % atom_or_identifier_term(identifier(IDName,_,_),IDName). | |
| 2764 | join_predicates(Op, TArgList, TBinaryP) :- | |
| 2765 | alloy_to_b_operator(Op, BOp), | |
| 2766 | ( BOp = conjunct | |
| 2767 | ; BOp = disjunct | |
| 2768 | ), | |
| 2769 | join_untyped_ast_nodes(BOp, TArgList, TBinaryP). | |
| 2770 | ||
| 2771 | join_untyped_ast_nodes(_, [], truth(none)). | |
| 2772 | join_untyped_ast_nodes(BOp, [H|T], Conjoined) :- | |
| 2773 | join_untyped_ast_nodes(BOp, T, H, Conjoined). | |
| 2774 | ||
| 2775 | join_untyped_ast_nodes(_, [], Acc, Acc). | |
| 2776 | join_untyped_ast_nodes(BOp, [H|T], Acc, Conjoined) :- | |
| 2777 | NewAcc =.. [BOp,none,Acc,H], | |
| 2778 | join_untyped_ast_nodes(BOp, T, NewAcc, Conjoined). | |
| 2779 | ||
| 2780 | ||
| 2781 | %:- load_files(library(system), [when(compile_time), imports([environ/2])]). | |
| 2782 | :- if(environ(prob_release,true)). | |
| 2783 | % Don't include tests in release mode. | |
| 2784 | :- else. | |
| 2785 | ||
| 2786 | :- use_module(library(plunit)). | |
| 2787 | :- use_module(testsrc(test_paths), []). % set up prob_examples(...) alias | |
| 2788 | ||
| 2789 | :- begin_tests(full_machine_translation). | |
| 2790 | ||
| 2791 | test(cards, []) :- | |
| 2792 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/cards.pl')). | |
| 2793 | ||
| 2794 | test(filesystem, []) :- | |
| 2795 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/filesystem.pl')). | |
| 2796 | ||
| 2797 | test(filesystem2, []) :- | |
| 2798 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/filesystem2.pl')). | |
| 2799 | ||
| 2800 | test(self_grandpas, []) :- | |
| 2801 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/selfgrandpas.pl')). | |
| 2802 | ||
| 2803 | test(queens, []) :- | |
| 2804 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/queens.pl')). | |
| 2805 | ||
| 2806 | test(queens2, []) :- | |
| 2807 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/queens2.pl')). | |
| 2808 | ||
| 2809 | test(queens3, []) :- | |
| 2810 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/queens3.pl')). | |
| 2811 | ||
| 2812 | test(queens4, []) :- | |
| 2813 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/queens4.pl')). | |
| 2814 | ||
| 2815 | test(river_crossing, []) :- | |
| 2816 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/rivercrossingpuzzle.pl')). | |
| 2817 | ||
| 2818 | test(river_crossing_v2, []) :- | |
| 2819 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/rivercrossingpuzzle_v2.pl')). | |
| 2820 | ||
| 2821 | test(enum_test, []) :- | |
| 2822 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/enumtest.pl')). | |
| 2823 | ||
| 2824 | test(disj_field_test, []) :- | |
| 2825 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/disjfieldtest.pl')). | |
| 2826 | ||
| 2827 | test(crewAlloc, []) :- | |
| 2828 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/crewalloc.pl')). | |
| 2829 | ||
| 2830 | test(http, []) :- | |
| 2831 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/http.pl')). | |
| 2832 | ||
| 2833 | test(knights, []) :- | |
| 2834 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/knights_and_knaves.pl')). | |
| 2835 | ||
| 2836 | test(join_binary, []) :- | |
| 2837 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/joinbinary.pl')). | |
| 2838 | ||
| 2839 | test(slot_data_v2, []) :- | |
| 2840 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/slot_data_v2.pl')). | |
| 2841 | ||
| 2842 | test(job_puzzle, []) :- | |
| 2843 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/job_puzzle.pl')). | |
| 2844 | ||
| 2845 | test(natural, []) :- | |
| 2846 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/natural.pl')). | |
| 2847 | ||
| 2848 | test(mutex,[]) :- | |
| 2849 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/mutex.pl')). | |
| 2850 | ||
| 2851 | test(family_v1,[]) :- | |
| 2852 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/family-v1.pl')). | |
| 2853 | ||
| 2854 | test(unary_ordering_rewriting, []) :- | |
| 2855 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/unary_ordering_rewriting.pl')). | |
| 2856 | ||
| 2857 | test(einstein1, []) :- | |
| 2858 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/einstein1.pl')). | |
| 2859 | ||
| 2860 | test(einstein2, []) :- | |
| 2861 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/einstein2.pl')). | |
| 2862 | ||
| 2863 | test(einstein3, []) :- | |
| 2864 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/einstein3.pl')). | |
| 2865 | ||
| 2866 | test(einsteins_enum, []) :- | |
| 2867 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/einsteins_enum.pl')). | |
| 2868 | ||
| 2869 | test(nodeweightedgraph, []) :- | |
| 2870 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/nodeweightedgraph.pl')). | |
| 2871 | ||
| 2872 | test(lists, []) :- | |
| 2873 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/lists.pl')). | |
| 2874 | ||
| 2875 | test(peano, []) :- | |
| 2876 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/peano.pl')). | |
| 2877 | ||
| 2878 | test(random_games, []) :- | |
| 2879 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/random_games.pl')). | |
| 2880 | ||
| 2881 | test(ordering_test, []) :- | |
| 2882 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/ordering_test.pl')). | |
| 2883 | ||
| 2884 | test(rellaws, []) :- | |
| 2885 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/rellaws.pl')). | |
| 2886 | ||
| 2887 | test(color_australia, []) :- | |
| 2888 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/color_australia.pl')). | |
| 2889 | ||
| 2890 | test(add_addr_correct, []) :- | |
| 2891 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/add_addr_correct.pl')). | |
| 2892 | ||
| 2893 | test(ambiguous_field_name, []) :- | |
| 2894 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/ambiguous_field_name.pl')). | |
| 2895 | ||
| 2896 | test(ambiguous_quantifier_field_name, []) :- | |
| 2897 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/ambiguous_quantifier_field_name.pl')). | |
| 2898 | ||
| 2899 | test(arithmetic, []) :- | |
| 2900 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/arithmetic.pl')). | |
| 2901 | ||
| 2902 | test(card, []) :- | |
| 2903 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/card.pl')). | |
| 2904 | ||
| 2905 | test(binary_differently_typed, []) :- | |
| 2906 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/binary_differently_typed.pl')). | |
| 2907 | ||
| 2908 | test(extendedfilesystem, []) :- | |
| 2909 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/extendedfilesystem.pl')). | |
| 2910 | ||
| 2911 | test(generated200, []) :- | |
| 2912 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/generated200.pl')). | |
| 2913 | ||
| 2914 | test(generated400, []) :- | |
| 2915 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/generated400.pl')). | |
| 2916 | ||
| 2917 | test(proofexample, []) :- | |
| 2918 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/proofexample.pl')). | |
| 2919 | ||
| 2920 | test(quantifiers, []) :- | |
| 2921 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/quantifiers.pl')). | |
| 2922 | ||
| 2923 | test(multiplicities, []) :- | |
| 2924 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/multiplicities.pl')). | |
| 2925 | ||
| 2926 | test(joinbinarycomplex, []) :- | |
| 2927 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/joinbinarycomplex.pl')). | |
| 2928 | ||
| 2929 | test(relations, []) :- | |
| 2930 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/relations.pl')). | |
| 2931 | ||
| 2932 | test(restrictions, []) :- | |
| 2933 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/restrictions.pl')). | |
| 2934 | ||
| 2935 | test(utilbool, []) :- | |
| 2936 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/utilbool.pl')). | |
| 2937 | ||
| 2938 | test(util_integer, []) :- | |
| 2939 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/util_integer.pl')). | |
| 2940 | ||
| 2941 | test(modulea, []) :- | |
| 2942 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/modulea.pl')). | |
| 2943 | ||
| 2944 | test(delundoesadd, []) :- | |
| 2945 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/delundoesadd.pl')). | |
| 2946 | ||
| 2947 | test(birthday, []) :- | |
| 2948 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/birthday.pl')). | |
| 2949 | ||
| 2950 | test(trivial_no_solution, []) :- | |
| 2951 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/trivial_no_solution.pl')). | |
| 2952 | ||
| 2953 | test(sets1, []) :- | |
| 2954 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/sets1.pl')). | |
| 2955 | ||
| 2956 | test(sets2, []) :- | |
| 2957 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/sets2.pl')). | |
| 2958 | ||
| 2959 | test(address_book, []) :- | |
| 2960 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/address_book.pl')). | |
| 2961 | ||
| 2962 | test(abstract_memory, []) :- | |
| 2963 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/abstract_memory.pl')). | |
| 2964 | ||
| 2965 | test(cache_memory, []) :- | |
| 2966 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/cache_memory.pl')). | |
| 2967 | ||
| 2968 | test(address_book_3a, []) :- | |
| 2969 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/address_book_3a.pl')). | |
| 2970 | ||
| 2971 | test(overlapping_ranges, []) :- | |
| 2972 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/overlapping_ranges.pl')). | |
| 2973 | ||
| 2974 | test(origin_tracking, []) :- | |
| 2975 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/origin_tracking.pl')). | |
| 2976 | ||
| 2977 | test(java_types, []) :- | |
| 2978 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/java_types.pl')). | |
| 2979 | ||
| 2980 | test(railway, []) :- | |
| 2981 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/railway.pl')). | |
| 2982 | ||
| 2983 | test(syllogism, []) :- | |
| 2984 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/syllogism.pl')). | |
| 2985 | ||
| 2986 | test(chord, []) :- | |
| 2987 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/chord.pl')). | |
| 2988 | ||
| 2989 | test(chord2, []) :- | |
| 2990 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/chord2.pl')). | |
| 2991 | ||
| 2992 | test(chord_bug_model, []) :- | |
| 2993 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/chord_bug_model.pl')). | |
| 2994 | ||
| 2995 | test(mark_sweep_gc, []) :- | |
| 2996 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/mark_sweep_gc.pl')). | |
| 2997 | ||
| 2998 | test(dijkstra_2_process, []) :- | |
| 2999 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/dijkstra_2_process.pl')). | |
| 3000 | ||
| 3001 | test(peterson, []) :- | |
| 3002 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/peterson.pl')). | |
| 3003 | ||
| 3004 | test(genealogy, []) :- | |
| 3005 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/genealogy.pl')). | |
| 3006 | ||
| 3007 | % wrong result for handshake, properties prevent finding a solution, probably caused by translation of 'one sig .. extends Person' | |
| 3008 | test(handshake, []) :- | |
| 3009 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/handshake.pl')). | |
| 3010 | ||
| 3011 | % error when setting up constants; argument of MU expression has more than one element | |
| 3012 | test(send_money, []) :- | |
| 3013 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/send_money.pl')). | |
| 3014 | % same as for send_money | |
| 3015 | test(four_bit_adder, []) :- | |
| 3016 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/4_bit_adder.pl')). | |
| 3017 | ||
| 3018 | test(farmer, []) :- | |
| 3019 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/farmer.pl')). | |
| 3020 | ||
| 3021 | test(ins, []) :- | |
| 3022 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/ins.pl')). | |
| 3023 | ||
| 3024 | test(ring_election1, []) :- | |
| 3025 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/ring_election1.pl')). | |
| 3026 | ||
| 3027 | test(ring_election2, []) :- | |
| 3028 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/ring_election2.pl')). | |
| 3029 | ||
| 3030 | test(com, []) :- | |
| 3031 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/com.pl')). | |
| 3032 | ||
| 3033 | test(paragraph_numbering, []) :- | |
| 3034 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/paragraph_numbering.pl')). | |
| 3035 | ||
| 3036 | %test(mark_sweep_gc2, []) :- | |
| 3037 | % load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/marksweepgc2.pl')). | |
| 3038 | ||
| 3039 | :- end_tests(full_machine_translation). | |
| 3040 | ||
| 3041 | :- endif. | |
| 3042 | % errors | |
| 3043 | /* | |
| 3044 | % translation failed for bijection_relation | |
| 3045 | test(ins_label, []) :- | |
| 3046 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/ins_label.pl')). | |
| 3047 | ||
| 3048 | % unknown identifier X in field while X_Sig exists | |
| 3049 | test(java_map, []) :- | |
| 3050 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/java_map.pl')). | |
| 3051 | % similar as above | |
| 3052 | test(firewire, []) :- | |
| 3053 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/firewire.pl')). | |
| 3054 | ||
| 3055 | % problems with ordering/next | |
| 3056 | test(view_backing, []) :- | |
| 3057 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/view_backing.pl')). | |
| 3058 | % similar as above | |
| 3059 | test(prisoners, []) :- | |
| 3060 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/prisoners.pl')). | |
| 3061 | ||
| 3062 | % missing translation for integer_sum | |
| 3063 | test(messaging, []) :- | |
| 3064 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/messaging.pl')). | |
| 3065 | ||
| 3066 | % Unknown identifier "this" in properties | |
| 3067 | test(hotel, []) :- | |
| 3068 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/hotel.pl')). | |
| 3069 | ||
| 3070 | test(p300_hotel, []) :- | |
| 3071 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/p300_hotel.pl')). | |
| 3072 | ||
| 3073 | test(flip_flop_state, []) :- | |
| 3074 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/flip_flop_state.pl')). | |
| 3075 | ||
| 3076 | test(reset_flip_flop_with_enable, []) :- | |
| 3077 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/reset_flip_flop_with_enable.pl')). | |
| 3078 | ||
| 3079 | % problem new remove this? singleton set problem with this | |
| 3080 | % but also uses unsupported module util/graph | |
| 3081 | test(dijkstra_k_state, []) :- | |
| 3082 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/dijkstra_k_state.pl')). | |
| 3083 | ||
| 3084 | % type errors, e.g., for bool'Not | |
| 3085 | test(ring_orientation, []) :- | |
| 3086 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/ring_orientation.pl')). | |
| 3087 | ||
| 3088 | %! An error occurred (source: type_error) ! | |
| 3089 | %! Type mismatch: Expected (((POW(Board)*INTEGER)*INTEGER)<->Queen), but was ((POW(Board)*INTEGER)<->(INTEGER*Queen)) in 'queens_Board' | |
| 3090 | %! Line: 7 Column: 16 until Line: 7 Column: 16 in file: alloytranslation | |
| 3091 | test(eight_queens, []) :- | |
| 3092 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/8_queens.pl')). | |
| 3093 | ||
| 3094 | % Could not infer type of _universe0 | |
| 3095 | test(java_types_soundness, []) :- | |
| 3096 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/java_types_soundness.pl')). | |
| 3097 | ||
| 3098 | test(sudoku1, []) :- | |
| 3099 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/sudoku1.pl')). | |
| 3100 | ||
| 3101 | test(sequence_test, []) :- | |
| 3102 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/sequence_test.pl')). | |
| 3103 | ||
| 3104 | test(seq_preconditions, []) :- | |
| 3105 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/seq_preconditions.pl')). | |
| 3106 | ||
| 3107 | test(hanoi, []) :- | |
| 3108 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/hanoi.pl')). | |
| 3109 | ||
| 3110 | test(directctrl,[]) :- | |
| 3111 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/directctrl.pl')). | |
| 3112 | ||
| 3113 | test(views,[]) :- | |
| 3114 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/views.pl')). | |
| 3115 | ||
| 3116 | % unsupported iden keyword in "in" | |
| 3117 | test(graphiso, []) :- | |
| 3118 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/graphiso.pl')). | |
| 3119 | ||
| 3120 | test(basic_auth, []) :- | |
| 3121 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/basic_auth.pl')). | |
| 3122 | ||
| 3123 | % Unknown identifier "univ" | |
| 3124 | test(properties, []) :- | |
| 3125 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/properties.pl')). | |
| 3126 | ||
| 3127 | % can probably not be translated due to univ | |
| 3128 | test(iolus, []) :- | |
| 3129 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/iolus.pl')). | |
| 3130 | test(distribution, []) :- | |
| 3131 | load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Prolog/distribution.pl')). | |
| 3132 | */ |