Allow #AG spec for bounded model checking (runtimeverification#458)

yzhang90 · dwightguth · commit 2669fd784f86 · 2019-05-10T10:29:56.000-05:00
* add dummy definition for allPathGlobally

* support #AG builtin

* add comment
diff --git a/k-distribution/include/builtin/kast.k b/k-distribution/include/builtin/kast.k
@@ -79,6 +79,8 @@ module ML-SYNTAX
              > K "#Implies" K [klabel(#Implies), symbol, mlOp, poly(0, 1, 2), format(%i%1%d%n%2%n%i%3%d)]
              > "#Exists" K "." K [klabel(#Exists), symbol, mlOp, poly(1; 0, 2), mlBinder]
              | "#Forall" K "." K [klabel(#Forall), symbol, mlOp, poly(1; 0, 2), mlBinder]
+             | "#AG" "(" K ")" [klabel(#AG), symbol, mlOp, poly(0, 1)]
+
 endmodule
 
 // To be used when parsing/pretty-printing symbolic configurations
diff --git a/k-distribution/include/kore/prelude.kore b/k-distribution/include/kore/prelude.kore
@@ -47,4 +47,9 @@ module K
   alias weakAlwaysFinally{A}(A) : A
   where weakAlwaysFinally{A}(X:A) := X:A []
 
+  // Definitions for CTL aliases
+  // Until we will have `mu` we resort to dummy definitions
+  alias allPathGlobally{A}(A) : A
+  where allPathGlobally{A}(X:A) := X:A []
+
 endmodule []
diff --git a/kernel/src/main/java/org/kframework/backend/kore/ConstructorChecks.java b/kernel/src/main/java/org/kframework/backend/kore/ConstructorChecks.java
@@ -80,7 +80,7 @@ public static boolean isBuiltinLabel(KLabel label) {
         return label.name().equals(KLabels.ML_FALSE.name()) || label.name().equals(KLabels.ML_TRUE.name()) || label.name().equals(KLabels.ML_NOT.name()) ||
                label.name().equals(KLabels.ML_OR.name()) || label.name().equals(KLabels.ML_AND.name()) || label.name().equals(KLabels.ML_IMPLIES.name()) ||
                label.name().equals(KLabels.ML_EQUALS.name()) || label.name().equals(KLabels.ML_CEIL.name()) || label.name().equals(KLabels.ML_FLOOR.name()) ||
-               label.name().equals(KLabels.ML_EXISTS.name()) || label.name().equals(KLabels.ML_FORALL.name());
+               label.name().equals(KLabels.ML_EXISTS.name()) || label.name().equals(KLabels.ML_FORALL.name()) || label.name().equals(KLabels.CTL_AG.name());
     }
 
     private boolean isBuiltinModuloConstructor(KLabel label) {
diff --git a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java b/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
@@ -1052,6 +1052,8 @@ private String convertBuiltinLabel(String klabel) {
         return "\\exists";
       case "#Forall":
         return "\\forall";
+      case "#AG":
+        return "allPathGlobally";
       default:
         throw KEMException.compilerError("Unsuppored kore connective in rule: " + klabel);
       }
diff --git a/kore/src/main/java/org/kframework/builtin/KLabels.java b/kore/src/main/java/org/kframework/builtin/KLabels.java
@@ -42,6 +42,7 @@ public class KLabels {
     public static final KLabel ML_IMPLIES = KLabel("#Implies");
     public static final KLabel ML_EXISTS = KLabel("#Exists");
     public static final KLabel ML_FORALL = KLabel("#Forall");
+    public static final KLabel CTL_AG = KLabel("#AG");
 
     public static final KLabel ListItem = KLabel("ListItem");
     public static final KLabel List = KLabel("_List_");

Original file line number	Diff line number	Diff line change
`@@ -80,7 +80,7 @@ public static boolean isBuiltinLabel(KLabel label) {`
`80`	`80`	`return label.name().equals(KLabels.ML_FALSE.name()) \|\| label.name().equals(KLabels.ML_TRUE.name()) \|\| label.name().equals(KLabels.ML_NOT.name()) \|\|`
`81`	`81`	`label.name().equals(KLabels.ML_OR.name()) \|\| label.name().equals(KLabels.ML_AND.name()) \|\| label.name().equals(KLabels.ML_IMPLIES.name()) \|\|`
`82`	`82`	`label.name().equals(KLabels.ML_EQUALS.name()) \|\| label.name().equals(KLabels.ML_CEIL.name()) \|\| label.name().equals(KLabels.ML_FLOOR.name()) \|\|`
`83`		`- label.name().equals(KLabels.ML_EXISTS.name()) \|\| label.name().equals(KLabels.ML_FORALL.name());`
	`83`	`+ label.name().equals(KLabels.ML_EXISTS.name()) \|\| label.name().equals(KLabels.ML_FORALL.name()) \|\| label.name().equals(KLabels.CTL_AG.name());`
`84`	`84`	`}`
`85`	`85`
`86`	`86`	`private boolean isBuiltinModuloConstructor(KLabel label) {`
Original file line number	Diff line number	Diff line change
`@@ -1052,6 +1052,8 @@ private String convertBuiltinLabel(String klabel) {`
`1052`	`1052`	`return "\\exists";`
`1053`	`1053`	`case "#Forall":`
`1054`	`1054`	`return "\\forall";`
	`1055`	`+ case "#AG":`
	`1056`	`+ return "allPathGlobally";`
`1055`	`1057`	`default:`
`1056`	`1058`	`throw KEMException.compilerError("Unsuppored kore connective in rule: " + klabel);`
`1057`	`1059`	`}`