From 12ebfbba9f10bb6648fb307dcb11430cf641864e Mon Sep 17 00:00:00 2001
From: rakhimov <ol.rakhimov@gmail.com>
Date: Tue, 31 Oct 2017 17:43:19 -0700
Subject: [PATCH] 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
---
 src/substitution.cc                           | 13 +++++++++-
 tests/initializer_tests.cc                    |  3 ++-
 .../substitution_nondeclarative_complex.xml   | 24 +++++++++++++++++++
 3 files changed, 38 insertions(+), 2 deletions(-)
 create mode 100644 tests/input/model/substitution_nondeclarative_complex.xml

diff --git a/src/substitution.cc b/src/substitution.cc
index 33f316ccc8..6462d8016b 100644
--- 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
index 2d547ba42d..9e743af87a 100644
--- 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
new file mode 100644
index 0000000000..4f249df556
--- /dev/null
+++ 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>