Restrict imperative Substitutions to AND/OR/NULL

Non-declarative substitutions have to be implemented with set operations at post-processing. Complex Boolean formulas would require more expensive solutions (i.e., solving the general satisfiability). The declarative substitutions, in contrast, can simply use implication operator at pre-processing, so there's no need to restrict formulas for the declarative approaches. Issue #154
rakhimov · Nov 1, 2017 · 12ebfbb · 12ebfbb
1 parent 2acd9e0
commit 12ebfbb
Show file tree

Hide file tree

Showing 3 changed files with 38 additions and 2 deletions.
diff --git a/src/substitution.cc b/src/substitution.cc
@@ -48,10 +48,21 @@ void Substitution::Validate() const {
     SCRAM_THROW(
         ValidityError("Substitution hypothesis formula cannot be nested."));
   }
-  if (source_.empty()) {
+  if (source_.empty()) {  // Declarative.
     const bool* constant = boost::get<bool>(&target_);
     if (constant && *constant)
       SCRAM_THROW(ValidityError("Substitution has no effect."));
+  } else {  // Non-declarative.
+    switch (hypothesis_->type()) {
+      case kNull:
+      case kAnd:
+      case kOr:
+        break;
+      default:
+        SCRAM_THROW(
+            ValidityError("Non-declarative substitution hypotheses only allow "
+                          "AND/OR/NULL connectives."));
+    }
   }
 }
 

diff --git a/tests/initializer_tests.cc b/tests/initializer_tests.cc
@@ -371,7 +371,8 @@ TEST(InitializerTest, IncorrectModelInputs) {
       "substitution_nested_formula.xml",
       "substitution_non_basic_event_formula.xml",
       "substitution_type_mismatch.xml",
-      "substitution_no_effect.xml"
+      "substitution_no_effect.xml",
+      "substitution_nondeclarative_complex.xml"
   };
 
   for (const auto& input : incorrect_inputs) {

diff --git a/tests/input/model/substitution_nondeclarative_complex.xml b/tests/input/model/substitution_nondeclarative_complex.xml
@@ -0,0 +1,24 @@
+<?xml version="1.0"?>
+<opsa-mef>
+  <define-substitution name="S">
+    <hypothesis>
+      <atleast min="2">
+        <event name="A"/>
+        <event name="B"/>
+        <event name="C"/>
+      </atleast>
+    </hypothesis>
+    <source>
+      <basic-event name="C"/>
+    </source>
+    <target>
+      <basic-event name="D"/>
+    </target>
+  </define-substitution>
+  <model-data>
+    <define-basic-event name="A"/>
+    <define-basic-event name="B"/>
+    <define-basic-event name="C"/>
+    <define-basic-event name="D"/>
+  </model-data>
+</opsa-mef>