From 7a3e79c1fef9c674ae9ca157dd8241eef41f6206 Mon Sep 17 00:00:00 2001
From: rakhimov <ol.rakhimov@gmail.com>
Date: Sat, 20 Jan 2018 07:11:42 -0800
Subject: [PATCH] Disallow arbitrarily nested Boolean formulae
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The MEF allows writing complex, nested Boolean formulae to define gates.
It is indeed very general and powerful,
but do the MEF and model developers need this power?
There is no reasoning in the standard justifying this complexity.

I can't find any FTA software currently supporting this MEF feature
except for SCRAM.
Having implemented this "feature" in SCRAM,
I concluded that this approach requires
a fundamentally different treatment of gates and input events.
It is peculiar to the MEF and confusing to users.
It is hard/impossible to represent graphically with traditional methods
without unconventional approaches
(phony gates/circuits/textual formula).

I reckon wiser people already avoid such complexity.
Excerpt from XFTA manual:
```
Nothing prevents to use nested formulae
(such as a ‘and’ of ‘or’ of events).
However, a best practice recommended by all safety standards is
to introduce an intermediary event per logical gate.
The only exception to this rule is negations,
as illustrated in our example...
```

Following the wisdom,
the MEF schema is modified to allow
only events or negations of events -- not formulas --
as Boolean formula arguments.
Note this only requires a schema/grammar change,
no specification wording is needed
because the original nested-formula is not specified in the first place.
---
 mef/schema/formula.rnc | 27 +++++++++++++++------------
 1 file changed, 15 insertions(+), 12 deletions(-)

diff --git a/mef/schema/formula.rnc b/mef/schema/formula.rnc
index 9d522ea..43722c3 100644
--- a/mef/schema/formula.rnc
+++ b/mef/schema/formula.rnc
@@ -1,23 +1,26 @@
 formula =
-  event
-  | Boolean-constant
-  | element and { formula+ }
-  | element or { formula+ }
-  | element not { formula }
-  | element xor { formula+ }
-  | element iff { formula+ }
-  | element nand { formula+ }
-  | element nor { formula+ }
+  argument
+  | element and { argument+ }
+  | element or { argument+ }
+  | element xor { argument+ }
+  | element iff { argument+ }
+  | element nand { argument+ }
+  | element nor { argument+ }
   | element atleast {
       attribute min { xsd:positiveInteger },
-      formula+
+      argument+
     }
   | element cardinality {
       attribute min { xsd:nonNegativeInteger },
       attribute max { xsd:nonNegativeInteger },
-      formula+
+      argument+
     }
-  | element imply { formula, formula }
+  | element imply { argument, argument }
+
+argument =
+  event
+  | element not { event }
+  | Boolean-constant
 
 event =
   element event {