Added Symbolic Strategy Functionality with SLUGS (UPDATED)

src/etc/jtlv/GROne/GROneMain.java

@@ -146,7 +146,7 @@ public static void main(String[] args) throws Exception {
             System.out.println("Specification is synthesizable!");
             System.out.println("====> Building an implementation...");
 
-            out_filename = out_filename_base + (opt_symbolic ? ".bdd" : ".aut");
+            out_filename = out_filename_base + (opt_symbolic ? ".add" : ".aut");
 
             tic = System.currentTimeMillis();		
 

src/lib/bdd.py

@@ -20,7 +20,7 @@
 #       - minimal Y after Z change
 
 class BDDStrategy(strategy.Strategy):
-    def __init__(self):
+    def __init__(self, add):
         super(BDDStrategy, self).__init__()
 
         # We will have a state collection just in order to provide a context
@@ -39,6 +39,9 @@ def __init__(self):
         # TODO: why is garbage collection crashing?? :( [e.g. on firefighting]
         self.mgr.DisableGarbageCollection()
 
+        # track if this is an add or bdd
+        self.add = add
+
     def _loadFromFile(self, filename):
         """
         Load in a strategy BDD from a file produced by a synthesizer,
@@ -50,20 +53,31 @@ def _loadFromFile(self, filename):
 
         a = pycudd.DdArray(1)
 
-        # Load in the actual BDD itself
-        # Note: We are using an ADD loader because the BDD loader
-        # would expect us to have a reduced BDD with only one leaf node
-        self.mgr.AddArrayLoad(pycudd.DDDMP_ROOT_MATCHLIST,
-                              None,
-                              pycudd.DDDMP_VAR_MATCHIDS,
-                              None,
-                              None,
-                              None,
-                              pycudd.DDDMP_MODE_TEXT,
-                              filename, None, a)
-
-        # Convert from a binary (0/1) ADD to a BDD
-        self.strategy = self.mgr.addBddPattern(a[0])
+        # Load in the actual BDD or ADD itself
+        if self.add:
+            # Note: We are using an ADD loader because the BDD loader
+            # would expect us to have a reduced BDD with only one leaf node
+            self.mgr.AddArrayLoad(pycudd.DDDMP_ROOT_MATCHLIST,
+                                  None,
+                                  pycudd.DDDMP_VAR_MATCHIDS,
+                                  None,
+                                  None,
+                                  None,
+                                  pycudd.DDDMP_MODE_TEXT,
+                                  filename, None, a)
+
+            # Convert from a binary (0/1) ADD to a BDD
+            self.strategy = self.mgr.addBddPattern(a[0])
+            logging.debug('ADD loaded')
+        else:
+            #try loading as BDD (input from SLUGS) instead of ADD (input from JTLV)
+            self.strategy  = self.mgr.BddLoad(pycudd.DDDMP_VAR_MATCHIDS,
+                                  None,
+                                  None,
+                                  None,
+                                  pycudd.DDDMP_MODE_TEXT,
+                                  filename, None)
+            logging.debug('BDD loaded')
 
         # Load in meta-data
         with open(filename, 'r') as f:

src/lib/project.py

@@ -246,7 +246,7 @@ def getStrategyFilename(self):
         """ Returns the full path of the file that should contain the strategy
             for this specification. """
 
-        return self.getFilenamePrefix() + ('.bdd' if self.compile_options["symbolic"] else '.aut')
+        return self.getFilenamePrefix() + ('.add' if (self.compile_options["symbolic"] and self.compile_options["synthesizer"].lower() == 'jtlv') else '.bdd' if (self.compile_options["symbolic"] and self.compile_options["synthesizer"].lower() == 'slugs') else '.aut')
 
 
 

src/lib/specCompiler.py

@@ -499,7 +499,7 @@ def _getSlugsCommand(self):
             # TODO: automatically compile for the user
             raise RuntimeError("Please compile the synthesis code first.  For instructions, see etc/slugs/README.md.")
 
-        cmd = [slugs_path, "--sysInitRoboticsSemantics", self.proj.getFilenamePrefix() + ".slugsin", self.proj.getFilenamePrefix() + ".aut"]
+        cmd = [slugs_path, "--sysInitRoboticsSemantics", self.proj.getFilenamePrefix() + ".slugsin"]
 
         return cmd
 
@@ -892,8 +892,12 @@ def _synthesizeAsync(self, log_function=None, completion_callback_function=None)
             cmd = self._getSlugsCommand()
 
             # Make sure flags are compatible
-            if any(self.proj.compile_options[k] for k in ("fastslow", "symbolic")):
-                raise RuntimeError("Slugs does not currently support fast/slow or symbolic compilation options.")
+            if self.proj.compile_options["fastslow"]:
+                raise RuntimeError("Slugs does not currently support fast/slow option.")
+            if self.proj.compile_options["symbolic"]:
+                cmd.extend(["--symbolicStrategy", self.proj.getFilenamePrefix() + ".bdd"])
+            else:
+                cmd.append(self.proj.getFilenamePrefix() + ".aut")
 
             # Create proper input for Slugs
             logging.info("Preparing Slugs input...")

src/lib/strategy.py

@@ -33,9 +33,12 @@ def createStrategyFromFile(filename, input_propositions, output_propositions):
     if filename.endswith(".aut"):
         import fsa
         new_strategy = fsa.FSAStrategy()
-    elif filename.endswith(".bdd"):
+    elif filename.endswith(".bdd") or filename.endswith(".add"):
         import bdd
-        new_strategy = bdd.BDDStrategy()
+        if filename.endswith(".bdd"):
+            new_strategy = bdd.BDDStrategy(add = False)
+        else:
+            new_strategy = bdd.BDDStrategy(add = True)
     else:
         raise ValueError("Unsupported strategy file type.  Filename must end with either '.aut' or '.bdd'.")