From a6a8a07c4329e047aa31d773c0b078d3758fefa2 Mon Sep 17 00:00:00 2001 From: wongkaiweng Date: Tue, 12 Aug 2014 12:15:08 -0400 Subject: [PATCH 1/2] add symoblic strategy option for slugs. Changed .bdd from jtlv to .add from clarification --- src/etc/jtlv/GROne/GROneMain.java | 2 +- src/lib/bdd.py | 44 ++++++++++++++++++++----------- src/lib/project.py | 2 +- src/lib/specCompiler.py | 10 ++++--- src/lib/strategy.py | 7 +++-- 5 files changed, 43 insertions(+), 22 deletions(-) diff --git a/src/etc/jtlv/GROne/GROneMain.java b/src/etc/jtlv/GROne/GROneMain.java index fb678934..685ddff7 100644 --- a/src/etc/jtlv/GROne/GROneMain.java +++ b/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(); diff --git a/src/lib/bdd.py b/src/lib/bdd.py index 8ab74d1b..634a9b6a 100644 --- a/src/lib/bdd.py +++ b/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: diff --git a/src/lib/project.py b/src/lib/project.py index e7980bd3..187a57d6 100644 --- a/src/lib/project.py +++ b/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') diff --git a/src/lib/specCompiler.py b/src/lib/specCompiler.py index 68b0e92b..8bd7202a 100644 --- a/src/lib/specCompiler.py +++ b/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...") diff --git a/src/lib/strategy.py b/src/lib/strategy.py index 27720297..6b406850 100755 --- a/src/lib/strategy.py +++ b/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'.") From 4988b5d3193dcccd3bda7f218f4c7dec493b5ff7 Mon Sep 17 00:00:00 2001 From: wongkaiweng Date: Tue, 12 Aug 2014 12:21:26 -0400 Subject: [PATCH 2/2] updated slugs to commit with symbolicStrategy fix --- src/etc/slugs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/etc/slugs b/src/etc/slugs index 57d9d992..17c3e87d 160000 --- a/src/etc/slugs +++ b/src/etc/slugs @@ -1 +1 @@ -Subproject commit 57d9d99242dfc59efe85c9a79441645249c775e8 +Subproject commit 17c3e87da99d7b6d81ee95f9eb82baf379ea8593