| summaryrefslogtreecommitdiff |
diff options
| -rw-r--r-- | Makefile | 34 | ||||
| -rw-r--r-- | ast-to-instr/Makefile | 59 | ||||
| -rw-r--r-- | ast-to-instr/src/Main.java | 11 | ||||
| -rw-r--r-- | ast-to-instr/src/OutputFile.java | 8 | ||||
| -rw-r--r-- | ast-to-instr/src/Parameters.java | 18 | ||||
| -rw-r--r-- | instr-to-kodkod/Makefile | 138 | ||||
| -rw-r--r-- | instr-to-kodkod/cfg-to-paths/Makefile (renamed from cfg-to-paths/Makefile) | 0 | ||||
| -rw-r--r-- | instr-to-kodkod/cfg-to-paths/src/ControlFlow.java (renamed from cfg-to-paths/src/ControlFlow.java) | 0 | ||||
| -rw-r--r-- | instr-to-kodkod/cfg-to-paths/src/Main.java (renamed from cfg-to-paths/src/Main.java) | 0 | ||||
| -rw-r--r-- | instr-to-kodkod/cfg-to-paths/src/Node.java (renamed from cfg-to-paths/src/Node.java) | 0 | ||||
| -rw-r--r-- | instr-to-kodkod/cfg-to-paths/src/Parameters.java (renamed from cfg-to-paths/src/Parameters.java) | 0 | ||||
| -rw-r--r-- | instr-to-kodkod/cfg-to-paths/src/Path.java (renamed from cfg-to-paths/src/Path.java) | 0 | ||||
| -rw-r--r-- | instr-to-kodkod/cfg-to-paths/src/QuickParser.java (renamed from cfg-to-paths/src/QuickParser.java) | 0 | ||||
| -rw-r--r-- | sol-pretty-printer/src/Main.java (renamed from sol_pretty_printer/src/Main.java) | 0 | ||||
| -rw-r--r-- | sol-pretty-printer/src/Models.java (renamed from sol_pretty_printer/src/Models.java) | 0 | ||||
| -rw-r--r-- | sol-pretty-printer/src/Parameters.java (renamed from sol_pretty_printer/src/Parameters.java) | 0 | ||||
| -rw-r--r-- | sol-pretty-printer/src/QuickParser.java (renamed from sol_pretty_printer/src/QuickParser.java) | 0 | ||||
| -rw-r--r-- | sol-pretty-printer/src/QuickSolParser.java (renamed from sol_pretty_printer/src/QuickSolParser.java) | 0 | ||||
| -rw-r--r-- | sol-pretty-printer/src/SolutionItem.java (renamed from sol_pretty_printer/src/SolutionItem.java) | 0 | ||||
| -rw-r--r-- | sol-pretty-printer/src/Solutions.java (renamed from sol_pretty_printer/src/Solutions.java) | 0 | ||||
| -rw-r--r-- | sol-pretty-printer/src/Strings.java (renamed from sol_pretty_printer/src/Strings.java) | 0 | ||||
| -rw-r--r-- | sol-pretty-printer/src/Waveforms.java (renamed from sol_pretty_printer/src/Waveforms.java) | 0 |
22 files changed, 201 insertions, 67 deletions
diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..4846880 --- /dev/null +++ b/Makefile @@ -0,0 +1,34 @@ +## Makefile Parameters ######################################################### +LEVEL_FILES = $(wildcard $(PWD)/data/level/*.lvl) +PROPERTY_FILES = $(wildcard $(PWD)/data/property/*.pro) +AST_FILE = $(PWD)/data/ast/best_chronometer_ever.xml + +TMP_DIR = /tmp/tabellion +MODEL_DIR = $(TMP_DIR)/mod +SOL_DIR = $(TMP_DIR)/sol + +## Sub-programs ################################################################ +AST_TO_INSTR = ast-to-instr +SOLVER = instr-to-kodkod +PRETTY_PRINTER = sol-pretty-printer + +export + +run: $(TMP_DIR) $(MODEL_DIR) $(SOL_DIR) + $(MAKE) -C $(AST_TO_INSTR) + $(MAKE) -C $(SOLVER) + $(MAKE) -C $(PRETTY_PRINTER) + +clean: + $(MAKE) -C $(AST_TO_INSTR) clean + $(MAKE) -C $(SOLVER) clean + $(MAKE) -C $(PRETTY_PRINTER) clean + +$(TMP_DIR): + mkdir -p $@ + +$(MODEL_DIR): + mkdir -p $@ + +$(SOL_DIR): + mkdir -p $@ diff --git a/ast-to-instr/Makefile b/ast-to-instr/Makefile index 4a19d4f..86a6d88 100644 --- a/ast-to-instr/Makefile +++ b/ast-to-instr/Makefile @@ -1,35 +1,60 @@ -INPUT_FILE = ../data/ast/best_chronometer_ever.xml +## Parameters ################################################################## +#### GHDL's xml AST output. +ifndef AST_FILE +AST_FILE = +endif + +#### Where to output the models. +ifndef MODEL_DIR +MODEL_DIR = +endif + +#### Binaries +###### JRE binary +ifndef JAVA +JAVA = java +endif -## Executables ################################################################# +###### JDK binary +ifndef JAVAC JAVAC = javac -JAVA = java -DOWNLOADER = wget +endif + +## Parameters Sanity Check ##################################################### +ifeq ($(strip $(AST_FILE)),) +$(error No AST_FILE defined as parameter.) +endif + +ifeq ($(strip $(MODEL_DIR)),) +$(error No output directory defined for the models.) +endif + +ifeq ($(strip $(JAVA)),) +$(error No Java executable defined as parameter.) +endif + +ifeq ($(strip $(JAVAC)),) +$(error No Java compiler defined as parameter.) +endif ## Java Config ################################################################# CLASSPATH = "./src/" -## Dependencies ################################################################ -JAR_SOURCE = https://noot-noot.org/onera_2017/jar/ -REQUIRED_JARS = - ## Makefile Magic ############################################################## SOURCES = $(wildcard src/*.java) CLASSES = $(SOURCES:.java=.class) ## Makefile Rules ############################################################## -all: structural.mod +$(MODEL_DIR)/structural.mod: $(CLASSES) $(AST_FILE) + $(JAVA) -cp $(CLASSPATH) Main $(AST_FILE) $(MODEL_DIR) clean: rm -f $(CLASSES) - rm -f *.mod - -structural.mod: $(CLASSES) $(REQUIRED_JARS) $(INPUT_FILE) - $(JAVA) -cp $(CLASSPATH) Main $(INPUT_FILE) + rm -f $(MODEL_DIR)/*.mod -%.class: %.java $(REQUIRED_JARS) +%.class: %.java $(JAVAC) -cp $(CLASSPATH) $< -%.jar: - echo "Attempting to download missing jar '$@'" - $(DOWNLOADER) "$(JAR_SOURCE)/$@" +$(MODEL_DIR): + mkdir -p $@ diff --git a/ast-to-instr/src/Main.java b/ast-to-instr/src/Main.java index 0e24f57..4f33ae1 100644 --- a/ast-to-instr/src/Main.java +++ b/ast-to-instr/src/Main.java @@ -55,11 +55,7 @@ public class Main return; } - MAIN_OUTPUT = - OutputFile.new_output_file - ( - PARAMETERS.get_main_output_filename() - ); + MAIN_OUTPUT = OutputFile.new_output_file("structural.mod"); try { @@ -176,4 +172,9 @@ public class Main { return MAIN_OUTPUT; } + + public static Parameters get_parameters () + { + return PARAMETERS; + } } diff --git a/ast-to-instr/src/OutputFile.java b/ast-to-instr/src/OutputFile.java index 42a6ad5..201ca2b 100644 --- a/ast-to-instr/src/OutputFile.java +++ b/ast-to-instr/src/OutputFile.java @@ -26,7 +26,13 @@ public class OutputFile { final OutputFile result; - result = new OutputFile(filename); + result = + new OutputFile + ( + Main.get_parameters().get_output_directory() + + "/" + + filename + ); ALL_OUTPUT_FILES.add(result); diff --git a/ast-to-instr/src/Parameters.java b/ast-to-instr/src/Parameters.java index 0407bb4..a7552d8 100644 --- a/ast-to-instr/src/Parameters.java +++ b/ast-to-instr/src/Parameters.java @@ -4,6 +4,7 @@ import java.util.ArrayList; public class Parameters { private final String xml_file; + private final String output_dir; private final boolean are_valid; @@ -13,27 +14,30 @@ public class Parameters ( "AST-to-Instr\n" + "USAGE:\n" - + "\tjava Main <XML_FILE>\n" + + "\tjava Main <XML_FILE> <OUTPUT_DIR>\n" + "PARAMETERS:\n" - + "\t- <XML_FILE>\tThe AST (XML format)." + + "\t- <XML_FILE>\tThe AST (XML format).\n" + + "\t- <OUTPUT_DIR>\tThe output directory (must already exist)." ); } public Parameters (String... args) { - if (args.length != 1) + if (args.length != 2) { print_usage(); xml_file = new String(); + output_dir = new String(); are_valid = false; return; } - are_valid = true; - xml_file = args[0]; + output_dir = args[1]; + + are_valid = true; } public String get_xml_file () @@ -41,9 +45,9 @@ public class Parameters return xml_file; } - public String get_main_output_filename() + public String get_output_directory () { - return "structural.mod"; + return output_dir; } public boolean are_valid () diff --git a/instr-to-kodkod/Makefile b/instr-to-kodkod/Makefile index 9823919..815c527 100644 --- a/instr-to-kodkod/Makefile +++ b/instr-to-kodkod/Makefile @@ -1,60 +1,124 @@ -## Target(s) Configuration ##################################################### -#MODEL_FILES = $(wildcard ../data/instructions/*.mod) -MODEL_FILES = \ - ../ast-to-instr/structural.mod \ - ../ast-to-instr/depths.mod \ - $(wildcard ../ast-to-instr/cfg_*.mod) \ - $(wildcard ../cfg-to-paths/*.mod) -MAP_FILES = $(wildcard ../ast-to-instr/*.map) -LEVEL_DIR = $(wildcard ../data/level/*.lvl) +## Parameters ################################################################## +#### Where to find the level files +ifndef LEVEL_FILES +LEVEL_FILES = +endif -PROPERTIES = $(wildcard ../data/property/cnes/*.pro) +#### Where to find the properties to verify +ifndef PROPERTY_FILES +PROPERTY_FILES = +endif -## Executables ################################################################# -JAVAC = javac +#### Where to find the model +ifndef MODEL_DIR +MODEL_DIR = +endif + +#### Where to store the CFG models +ifndef CFG_MODEL_DIR +CFG_MODEL_DIR = $(MODEL_DIR)/cfg/ +endif + +#### Where to output the solutions. +ifndef SOL_DIR +SOL_DIR = +endif + +#### Where to get the missing Jar files. +ifndef JAR_SOURCE +JAR_SOURCE = "https://noot-noot.org/tabellion/jar/" +endif + +#### Binaries +###### JRE binary +ifndef JAVA JAVA = java +endif + +###### JDK binary +ifndef JAVAC +JAVAC = javac +endif + +##### Downloader +ifndef DOWNLOADER DOWNLOADER = wget +endif -## Java Config ################################################################# -CLASSPATH = "kodkod.jar:./src/:./parser/:org.sat4j.core.jar:antlr-4.7-complete.jar" +## Parameters Sanity Check ##################################################### +ifeq ($(strip $(LEVEL_FILES)),) +$(error No LEVEL_FILES defined as parameter.) +endif + +ifeq ($(strip $(PROPERTY_FILES)),) +$(error No PROPERTY_FILES defined as parameter.) +endif + +ifeq ($(strip $(MODEL_DIR)),) +$(error No MODEL_DIR defined as parameter.) +endif + +ifeq ($(strip $(CFG_MODEL_DIR)),) +$(error No CFG_MODEL_DIR defined as parameter.) +endif -## Dependencies ################################################################ -JAR_SOURCE = https://noot-noot.org/onera_2017/jar/ +ifeq ($(strip $(SOL_DIR)),) +$(error No SOL_DIR defined as parameter.) +endif + +ifeq ($(strip $(JAR_SOURCE)),) +$(error No JAR_SOURCE defined as parameter.) +endif + +ifeq ($(strip $(JAVA)),) +$(error No Java executable defined as parameter.) +endif + +ifeq ($(strip $(JAVAC)),) +$(error No Java compiler defined as parameter.) +endif + +ifeq ($(strip $(DOWNLOADER)),) +$(error No Java executable defined as parameter.) +endif + +################################################################################ +CLASSPATH = "kodkod.jar:./src/:./parser/:org.sat4j.core.jar:antlr-4.7-complete.jar" REQUIRED_JARS = kodkod.jar org.sat4j.core.jar antlr-4.7-complete.jar ## Makefile Magic ############################################################## -GLOBAL_INPUT_FILES = $(MODEL_FILES) $(LEVEL_DIR) $(MAP_FILES) -SOURCES = $(wildcard src/*.java parser/*.java) -GRAMMARS = $(wildcard parser/*.g4) +SOURCES = $(wildcard src/*.java) CLASSES = $(SOURCES:.java=.class) -SOLUTIONS = $(PROPERTIES:.pro=.sol) +SOLUTION_FILES = $(addprefix $(SOL_DIR)/,$(notdir $(PROPERTY_FILES:.pro=.sol))) +MODEL_FILES = \ + $(MODEL_DIR)/structural.mod \ + $(filter-out %structural.mod,$(wildcard $(MODEL_DIR)/*.mod)) +export ## Makefile Rules ############################################################## -run: $(SOLUTIONS) +run: cfg-generator parser $(SOLUTION_FILES) + +cfg-generator: + $(MAKE) -C cfg-to-paths -all: parser/PropertyParser.java $(CLASSES) +parser: antlr-4.7-complete.jar $(MAKE) -C parser - $(MAKE) -C ../ast-to-instr - $(MAKE) -C ../cfg-to-paths clean: - rm -f $(CLASSES) $(MAKE) -C parser clean - $(MAKE) -C ../ast-to-instr clean - $(MAKE) -C ../cfg-to-paths clean + $(MAKE) -C cfg-to-paths clean + rm -f $(CLASSES) -%.sol: %.pro parser/PropertyParser.java $(CLASSES) $(REQUIRED_JARS) - echo "Solving \"$<\"..." - $(MAKE) -C ../ast-to-instr - $(MAKE) -C ../cfg-to-paths - $(JAVA) -cp $(CLASSPATH) Main $@ $< $(GLOBAL_INPUT_FILES) -v +%.sol: cfg-generator parser $(CLASSES) $(PROPERTY_FILES) $(MODEL_FILES) $(LEVEL_FILES) + $(JAVA) -cp $(CLASSPATH) Main $@ \ + $(filter %$(basename $(notdir $@)).pro,$(PROPERTY_FILES)) \ + $(LEVEL_FILES) \ + $(MODEL_FILES) + -v -%.class: %.java $(REQUIRED_JARS) parser/PropertyParser.java +%.class: %.java $(REQUIRED_JARS) parser $(JAVAC) -cp $(CLASSPATH) $< %.jar: - echo "Attempting to download missing jar '$@'" + echo "Attempting to download missing jar '$@'..." $(DOWNLOADER) "$(JAR_SOURCE)/$@" - -parser/PropertyParser.java: antlr-4.7-complete.jar $(GRAMMAR) - $(MAKE) -C parser diff --git a/cfg-to-paths/Makefile b/instr-to-kodkod/cfg-to-paths/Makefile index c9d14be..c9d14be 100644 --- a/cfg-to-paths/Makefile +++ b/instr-to-kodkod/cfg-to-paths/Makefile diff --git a/cfg-to-paths/src/ControlFlow.java b/instr-to-kodkod/cfg-to-paths/src/ControlFlow.java index 93d20ba..93d20ba 100644 --- a/cfg-to-paths/src/ControlFlow.java +++ b/instr-to-kodkod/cfg-to-paths/src/ControlFlow.java diff --git a/cfg-to-paths/src/Main.java b/instr-to-kodkod/cfg-to-paths/src/Main.java index d5cc650..d5cc650 100644 --- a/cfg-to-paths/src/Main.java +++ b/instr-to-kodkod/cfg-to-paths/src/Main.java diff --git a/cfg-to-paths/src/Node.java b/instr-to-kodkod/cfg-to-paths/src/Node.java index 3b6f2c1..3b6f2c1 100644 --- a/cfg-to-paths/src/Node.java +++ b/instr-to-kodkod/cfg-to-paths/src/Node.java diff --git a/cfg-to-paths/src/Parameters.java b/instr-to-kodkod/cfg-to-paths/src/Parameters.java index 91303d2..91303d2 100644 --- a/cfg-to-paths/src/Parameters.java +++ b/instr-to-kodkod/cfg-to-paths/src/Parameters.java diff --git a/cfg-to-paths/src/Path.java b/instr-to-kodkod/cfg-to-paths/src/Path.java index 9e0897f..9e0897f 100644 --- a/cfg-to-paths/src/Path.java +++ b/instr-to-kodkod/cfg-to-paths/src/Path.java diff --git a/cfg-to-paths/src/QuickParser.java b/instr-to-kodkod/cfg-to-paths/src/QuickParser.java index 47cea27..47cea27 100644 --- a/cfg-to-paths/src/QuickParser.java +++ b/instr-to-kodkod/cfg-to-paths/src/QuickParser.java diff --git a/sol_pretty_printer/src/Main.java b/sol-pretty-printer/src/Main.java index 7a7bfcd..7a7bfcd 100644 --- a/sol_pretty_printer/src/Main.java +++ b/sol-pretty-printer/src/Main.java diff --git a/sol_pretty_printer/src/Models.java b/sol-pretty-printer/src/Models.java index 097e76f..097e76f 100644 --- a/sol_pretty_printer/src/Models.java +++ b/sol-pretty-printer/src/Models.java diff --git a/sol_pretty_printer/src/Parameters.java b/sol-pretty-printer/src/Parameters.java index 92e9074..92e9074 100644 --- a/sol_pretty_printer/src/Parameters.java +++ b/sol-pretty-printer/src/Parameters.java diff --git a/sol_pretty_printer/src/QuickParser.java b/sol-pretty-printer/src/QuickParser.java index 19d29e7..19d29e7 100644 --- a/sol_pretty_printer/src/QuickParser.java +++ b/sol-pretty-printer/src/QuickParser.java diff --git a/sol_pretty_printer/src/QuickSolParser.java b/sol-pretty-printer/src/QuickSolParser.java index e162096..e162096 100644 --- a/sol_pretty_printer/src/QuickSolParser.java +++ b/sol-pretty-printer/src/QuickSolParser.java diff --git a/sol_pretty_printer/src/SolutionItem.java b/sol-pretty-printer/src/SolutionItem.java index f251b62..f251b62 100644 --- a/sol_pretty_printer/src/SolutionItem.java +++ b/sol-pretty-printer/src/SolutionItem.java diff --git a/sol_pretty_printer/src/Solutions.java b/sol-pretty-printer/src/Solutions.java index 38a426a..38a426a 100644 --- a/sol_pretty_printer/src/Solutions.java +++ b/sol-pretty-printer/src/Solutions.java diff --git a/sol_pretty_printer/src/Strings.java b/sol-pretty-printer/src/Strings.java index 31f6145..31f6145 100644 --- a/sol_pretty_printer/src/Strings.java +++ b/sol-pretty-printer/src/Strings.java diff --git a/sol_pretty_printer/src/Waveforms.java b/sol-pretty-printer/src/Waveforms.java index 3a40869..3a40869 100644 --- a/sol_pretty_printer/src/Waveforms.java +++ b/sol-pretty-printer/src/Waveforms.java |