From bc8e275546e2e6fe6bcf19ce42c0fab07eecdf4c Mon Sep 17 00:00:00 2001
From: Nathanael Sensfelder <SpamShield0@MultiAgentSystems.org>
Date: Mon, 31 Jul 2017 17:04:51 +0200
Subject: Fixes typo with functions, errors in grammar.

Looking for the groups matching CNE_01700 appears to take a really long
time. The formula is quite complex, yet unlikely to be one of the most
complex ones, so we'll have to see what can be done.
---
 instr-to-kodkod/Makefile                 | 5 ++---
 instr-to-kodkod/parser/PropertyLexer.g4  | 4 ++--
 instr-to-kodkod/parser/PropertyParser.g4 | 7 ++++++-
 instr-to-kodkod/src/Parameters.java      | 2 +-
 4 files changed, 11 insertions(+), 7 deletions(-)

(limited to 'instr-to-kodkod')

diff --git a/instr-to-kodkod/Makefile b/instr-to-kodkod/Makefile
index bdc7324..5d81814 100644
--- a/instr-to-kodkod/Makefile
+++ b/instr-to-kodkod/Makefile
@@ -9,8 +9,7 @@ MAP_FILES = $(wildcard ../ast-to-instr/*.map)
 LEVEL_DIR = $(wildcard ../data/level/*.lvl)
 
 PROPERTIES = \
-	../data/property/combinational_processes.pro \
-	../data/property/likely_a_clock.pro
+	../data/property/cnes/CNE_01700.pro
 
 ## Executables #################################################################
 JAVAC = javac
@@ -49,7 +48,7 @@ clean:
 	echo "Solving \"$<\"..."
 	$(MAKE) -C ../ast-to-instr
 	$(MAKE) -C ../cfg-to-paths
-	$(JAVA) -cp $(CLASSPATH) Main $@ $< $(GLOBAL_INPUT_FILES)
+	$(JAVA) -cp $(CLASSPATH) Main $@ $< $(GLOBAL_INPUT_FILES) -v
 
 %.class: %.java $(REQUIRED_JARS) parser/PropertyParser.java
 	$(JAVAC) -cp $(CLASSPATH) $<
diff --git a/instr-to-kodkod/parser/PropertyLexer.g4 b/instr-to-kodkod/parser/PropertyLexer.g4
index ec01c88..f5b553e 100644
--- a/instr-to-kodkod/parser/PropertyLexer.g4
+++ b/instr-to-kodkod/parser/PropertyLexer.g4
@@ -4,8 +4,8 @@ fragment SEP: [ \t\r\n]+;
 
 L_PAREN : '(';
 R_PAREN : ')';
-L_BRAKT: ']';
-R_BRAKT: '[';
+L_BRAKT: '[';
+R_BRAKT: ']';
 
 TAG_EXISTING_KW: '(tag_existing' SEP;
 
diff --git a/instr-to-kodkod/parser/PropertyParser.g4 b/instr-to-kodkod/parser/PropertyParser.g4
index 3e5634f..e6cd164 100644
--- a/instr-to-kodkod/parser/PropertyParser.g4
+++ b/instr-to-kodkod/parser/PropertyParser.g4
@@ -323,7 +323,7 @@ regex_special_predicate [Variable current_node]
 
    (WS)* REGEX_SPECIAL_PREDICATE_KW
       id_or_string_or_fun[current_node]
-      STRING
+   (WS)+ STRING
    (WS)* R_PAREN
 
    {
@@ -1303,6 +1303,11 @@ formula [Variable current_node]
       $result = ($predicate.result);
    }
 
+   | regex_special_predicate[current_node]
+   {
+      $result = ($regex_special_predicate.result);
+   }
+
    | and_operator[current_node]
    {
       $result = ($and_operator.result);
diff --git a/instr-to-kodkod/src/Parameters.java b/instr-to-kodkod/src/Parameters.java
index 7c80474..c6383bd 100644
--- a/instr-to-kodkod/src/Parameters.java
+++ b/instr-to-kodkod/src/Parameters.java
@@ -140,7 +140,7 @@ public class Parameters
                prop_file = args[i];
             }
          }
-         else if (output_file.equals("-v") || output_file.equals("--verbose"))
+         else if (args[i].equals("-v") || args[i].equals("--verbose"))
          {
             should_be_verbose = true;
          }
-- 
cgit v1.2.3-70-g09d2