Change actuator mutex to include initial conditions.

ltlbroom/ltl.py

@@ -80,10 +80,10 @@ def next_(text):
 
 def mutex_(items, include_all_off=False):
     """Create a system proposition mutex over the given items."""
-    return always(or_([and_([item1] +
-                            [not_(item2) for item2 in items if item2 != item1])
-                       for item1 in items] +
-                      ([and_([not_(item) for item in items])] if include_all_off else [])))
+    return or_([and_([item1] +
+                     [not_(item2) for item2 in items if item2 != item1])
+                for item1 in items] +
+               ([and_([not_(item) for item in items])] if include_all_off else []))
 
 
 def iff(prop1, prop2):

ltlbroom/specgeneration.py

@@ -181,10 +181,11 @@ def generate(self, text, sensors, regions, props, tag_dict, realizable_reactions
 
         # Add the actuator mutex
         if len(self.props) > 1:
+            actuator_mutex = mutex_([sys_(prop) for prop in self.props], True)
             generation_trees["Safety assumptions"] = \
                 {"Safety assumptions":
                  [SpecChunk("Robot can perform only one action at a time.",
-                            [mutex_([sys_(prop) for prop in self.props], True)],
+                            [actuator_mutex, always(actuator_mutex)],
                             SpecChunk.SYS, None)]}
 
         for line in text.split('\n'):