diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml index 24e1876a48b562bd9c1d2ca7c718a280fca362d8..56f2d69b0424296c4fab2843c00659c240210c90 100644 --- a/src/plugins/aorai/data_for_aorai.ml +++ b/src/plugins/aorai/data_for_aorai.ml @@ -1536,9 +1536,28 @@ let type_cond_auto auto = { original_auto with states = List.rev states; trans = List.rev trans } +(* Check Metavariable compatibility *) +let checkMetavariableCompatibility auto = + let is_extended_trans trans = + match trans.cross with + | Otherwise -> false + | Seq [ elt ] -> + elt.nested <> [] || not (is_single elt) + | Seq _ -> true + in + let has_metavariables = not (Datatype.String.Map.is_empty auto.metavariables) + and deterministic = Aorai_option.Deterministic.get () + and uses_extended_guards = List.exists is_extended_trans auto.trans in + if has_metavariables && (not deterministic || uses_extended_guards) then + Aorai_option.abort + "The use of metavariables is incompatible with non-deterministic \ + automata, such as automa using extended transitions." + + (** Stores the buchi automaton and its variables and functions as it is returned by the parsing *) let setAutomata auto = + checkMetavariableCompatibility auto; let auto = type_cond_auto auto in automata:=Some auto; check_states "typed automata"; diff --git a/src/plugins/aorai/tests/ya/metavariables-incompatible.i b/src/plugins/aorai/tests/ya/metavariables-incompatible.i new file mode 100644 index 0000000000000000000000000000000000000000..e572c48469923c88a149cdb6ca58f6d2130f48cd --- /dev/null +++ b/src/plugins/aorai/tests/ya/metavariables-incompatible.i @@ -0,0 +1,6 @@ +/* run.config* + OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/aorai/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@ +*/ + +void main(void) {} + diff --git a/src/plugins/aorai/tests/ya/metavariables-incompatible.ya b/src/plugins/aorai/tests/ya/metavariables-incompatible.ya new file mode 100644 index 0000000000000000000000000000000000000000..059f0d555ba7fa97e2d82f9988a895f06b968132 --- /dev/null +++ b/src/plugins/aorai/tests/ya/metavariables-incompatible.ya @@ -0,0 +1,9 @@ +%init: a; +%accept: b; +%deterministic; + +$x : int; + +a : { CALL(main)* } -> b; + +b : -> b; diff --git a/src/plugins/aorai/tests/ya/oracle/metavariables-incompatible.res.oracle b/src/plugins/aorai/tests/ya/oracle/metavariables-incompatible.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..cba15445f484ec9234cf849631720bcbb4fe69e7 --- /dev/null +++ b/src/plugins/aorai/tests/ya/oracle/metavariables-incompatible.res.oracle @@ -0,0 +1,4 @@ +[kernel] Parsing tests/aorai/metavariables-incompatible.i (no preprocessing) +[aorai] Welcome to the Aorai plugin +[aorai] User Error: The use of metavariables is incompatible with non-deterministic automata, such as automa using extended transitions. +[kernel] Plug-in aorai aborted: invalid user input.