Core-finding

src/etc/jtlv/GROne/GROneDebug.java

@@ -36,12 +36,17 @@ public static void main(String[] args) throws Exception {
 
         // Check that we have enough arguments
         // This class takes the same arguments as GROneMain.
-		if (args.length < 2) {
+	if (args.length < 2) {
             System.err.println("Usage: java GROneDebug [smv_file] [ltl_file]");
             System.exit(1);
         }
-
-        Env.loadModule(args[0]);
+
+	boolean refine = false;
+	if (args.length == 3) {
+            refine =  Boolean.parseBoolean(args[2]);
+        }
+
+	Env.loadModule(args[0]);
         Spec[] spcs = Env.loadSpecFile(args[1]);
 
         // Figure out the name of our output file by stripping the spec filename extension and adding .aut
@@ -61,8 +66,13 @@ public static void main(String[] args) throws Exception {
 
 
 		//Prints the results of analyzing the specification. 
-		System.out.println(analyze(env, sys));		
+		if (!refine) {
+			System.out.println(analyze(env, sys));
+		} else {
+			System.out.println(refine(env, sys, args));
+		}
 	}
+
 
 	public static String analyze(SMVModule env, SMVModule sys) {
 
@@ -175,10 +185,19 @@ public static String analyze(SMVModule env, SMVModule sys) {
 		}catch (Exception e){//Catch exception if any
 			      System.err.println("Error: " + e.getMessage());
 		}
-
+
+		if (debugInfo.contains("System highlighted goal")) {
+			explainSys = 1;
+		}
+		if (debugInfo.contains("Environment highlighted goal")) {
+			explainEnv = 1;
+		}
+
 		return debugInfo;
 	}
 
+
+
 	public static class NOPPrintStream extends PrintStream
 	{
 	    public NOPPrintStream() { super((OutputStream)null); }
@@ -290,4 +309,14 @@ else if ((sys.trans().and(Env.prime(sys.justiceAt(i-1))).isZero()) | sys.trans()
 		}
 		return debugInfo;
 	}
+
+	public static String refine(SMVModule env, SMVModule sys, String[] args) {
+		String result = "";
+		try{
+			result += "Guilty safety conjuncts are " + SpecSubsets.iteratedCoreSafetyIndices(args);
+		}catch (Exception e){//Catch exception if any
+			System.err.println("Error: " + e.getMessage());
+		}
+		return result;
+	}
 }

src/etc/jtlv/GROne/GROneGame.java

@@ -1270,7 +1270,9 @@ public boolean calculate_counterstrategy(BDD ini, boolean enable_234, boolean de
 
                 //when detecting system unsatisfiability, all env actions in primed_cur_succ (which is actualy Env.TRUE() in the nondet case) should be valid
 				//result = result & (input.equals(p_st.and(env.trans())));
-				result = result & (input.equals(p_st.and(primed_cur_succ)));
+				//System.out.println("Input= "+input);
+				//System.out.println("Possibilities= "+p_st.and(primed_cur_succ));
+				result = result & (input.equals(p_st.and(env.trans())));
                 if (!result && !det) break;
 				//result is true if for every state, all environment actions take us into a lower iterate of Z
 				//this means the environment can do anything to prevent the system from achieving some goal.

src/etc/jtlv/GROne/SpecSubsets.java

@@ -0,0 +1,208 @@
+import net.sf.javabdd.BDD;
+import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.LinkedList;
+import java.util.List;
+import edu.wis.jtlv.env.Env;
+import edu.wis.jtlv.env.module.SMVModule;
+import edu.wis.jtlv.env.spec.Spec;
+import edu.wis.jtlv.env.spec.Operator;
+import edu.wis.jtlv.env.spec.SpecBDD;
+import edu.wis.jtlv.env.spec.SpecExp;
+
+public class SpecSubsets {
+    public enum ConjunctType {
+        INITIAL, SAFETY, LIVENESS, OTHER;
+    }
+
+	public static void main(String[] args) throws Exception {
+        // Check that we have enough arguments
+        if (args.length < 2) {
+            System.err.println("Usage: java SpecSubsets <smv_file> <ltl_file>");
+            System.exit(1);
+        }                
+
+        // Load SMV and LTL files
+        Env.loadModule(args[0]);
+        Spec[] spcs = Env.loadSpecFile(args[1]);
+
+        // Parse the specs
+		Spec[] e_conjuncts = GROneParser.parseConjuncts(spcs[0]);
+		Spec[] s_conjuncts = GROneParser.parseConjuncts(spcs[1]);
+
+        // Load all of the environment spec
+		SMVModule m_env = (SMVModule) Env.getModule("main.e");
+		GROneParser.addReactiveBehavior(m_env, e_conjuncts);
+
+		SMVModule m_sys = (SMVModule) Env.getModule("main.s");
+        // Load all of the system initials and goals
+        GROneParser.addReactiveBehavior(m_sys, getConjunctsByType(s_conjuncts, ConjunctType.INITIAL));
+        GROneParser.addReactiveBehavior(m_sys, getConjunctsByType(s_conjuncts, ConjunctType.LIVENESS));
+
+        m_sys.initial().printSet();
+
+        // Incrementally load the system safeties
+        for (Spec safety_conjunct : getConjunctsByType(s_conjuncts, ConjunctType.SAFETY)) {
+            clearSpecPartFromModule(m_sys, ConjunctType.SAFETY); // Remove this line if you want to accumulate
+            System.out.println("Adding " + safety_conjunct);
+            GROneParser.addReactiveBehavior(m_sys, new Spec[]{safety_conjunct});
+            m_sys.trans().printSet();
+            System.out.println("=====================================");
+        }
+	}
+
+    public static String iteratedCoreSafetyIndices (String[] args) throws Exception {
+	return (iteratedCoreSafetyIndices (args, false));
+    }
+
+    public static String iteratedCoreSafetyIndices (String[] args, boolean verbose) throws Exception {
+
+        // Check that we have enough arguments
+        if (args.length < 2) {
+            System.err.println("Usage: java SpecSubsets <smv_file> <ltl_file>");
+            System.exit(1);
+        }                
+
+        // Load SMV and LTL files
+        Spec[] spcs = Env.loadSpecFile(args[1]);
+
+        // Parse the specs
+		Spec[] e_conjuncts = GROneParser.parseConjuncts(spcs[0]);
+		Spec[] s_conjuncts = GROneParser.parseConjuncts(spcs[1]);
+
+        // Load all of the environment spec
+		SMVModule m_env = (SMVModule) Env.getModule("main.e");
+		GROneParser.addReactiveBehavior(m_env, e_conjuncts);
+
+		SMVModule m_sys = (SMVModule) Env.getModule("main.s");
+        // Load all of the system initials and goals
+        GROneParser.addReactiveBehavior(m_sys, getConjunctsByType(s_conjuncts, ConjunctType.INITIAL));
+        GROneParser.addReactiveBehavior(m_sys, getConjunctsByType(s_conjuncts, ConjunctType.LIVENESS));
+
+	Spec[] all_safeties = getConjunctsByType(s_conjuncts, ConjunctType.SAFETY);
+	GROneParser.addReactiveBehavior(m_sys, all_safeties);
+
+
+
+	BDD all_init = m_sys.initial().and(m_env.initial());
+	if (verbose) {
+	    System.out.println("Initial Conditions " + all_init);
+	    System.out.println("Full safety specification " + m_sys.trans());
+	}
+
+
+	BDD counter_exmple;
+	GROneGame g;
+
+
+	int i = 0;
+	int j = 0;
+
+
+	List<Integer> list = new LinkedList<Integer>();
+	for (int k = 0; k <all_safeties.length; k++) {
+	    list.add(k);
+	}
+
+	//populate list of core candidates with all conjuncts
+	ArrayList<Integer> candidates = new ArrayList<Integer>(list);
+
+
+        // Remove the system safeties one at a time
+        for (Spec safety_conjunct : all_safeties) {
+	    if (verbose) System.out.println("Removing conjunct " + i + " = " + safety_conjunct);
+	    clearSpecPartFromModule(m_sys, ConjunctType.SAFETY); 
+	    j = 0;
+	    for (Spec safety_conjunct2 : all_safeties) {
+		//add only those conjuncts that are being considered, excluding the current conjunct
+	    	if (i != j && candidates.contains(new Integer(j))) {
+		    GROneParser.addReactiveBehavior(m_sys, new Spec[]{safety_conjunct2});
+		}
+		j++;
+	    }
+
+	    //check synthesizability
+	    g = new GROneGame(m_env,m_sys);
+	    counter_exmple = g.envWinningStates().and(all_init);
+	    //if removing this conjunct has made the specification synthesizable, add it back in
+	    if (counter_exmple.isZero()) {
+		if (verbose) System.out.println("Added it back in" + safety_conjunct);
+	    } else {
+		//this is no longer a candidate guilty conjunct
+		candidates.remove(new Integer(i));
+	    }
+	    if (verbose) System.out.println("=====================================");
+            i++;
+        }
+
+	int[] ret = new int[candidates.size()];
+	for(int n = 0;n < ret.length;n++) {
+	  ret[n] = ((Integer)candidates.get(n)).intValue();
+	}
+	return Arrays.toString(ret);
+    }
+
+    public static Spec[] getConjunctsByType(Spec[] sp, ConjunctType t) throws Exception {
+        ArrayList<Spec> conjuncts = new ArrayList<Spec>();
+
+        for (Spec conjunct : sp) {
+            if (getConjunctType(conjunct) == t) {
+                conjuncts.add(conjunct);
+            }
+        }
+
+        return conjuncts.toArray(new Spec[0]);
+    }
+
+    public static String getOutermostTemporalOperators(Spec sp) throws Exception {
+        // Stop recursion when we reach a pure BDD
+        if (sp instanceof SpecBDD) {
+            return "";
+        }
+
+        // This should never happen
+        if (!(sp instanceof SpecExp)) {
+            throw new Exception("Encountered subconjunct that is neither SpecBDD or SpecExp");
+        }
+
+        // Cast to SpecExp
+        SpecExp spe = (SpecExp) sp;
+
+        // Add the temporal operator we see and recurse
+        if (spe.getOperator() == Operator.GLOBALLY) {
+            return "G" + getOutermostTemporalOperators(spe.getChildren()[0]);
+        } else if (spe.getOperator() == Operator.FINALLY) {
+            return "F" + getOutermostTemporalOperators(spe.getChildren()[0]);
+        } else {
+            throw new Exception("Encountered SpecExp that is neither GLOBALLY or FINALLY");
+        }
+    }
+
+    public static ConjunctType getConjunctType(Spec sp) throws Exception {
+        String operators = getOutermostTemporalOperators(sp);
+
+        if (operators.equals("")) {
+            return ConjunctType.INITIAL;
+        } else if (operators.equals("G")) {
+            return ConjunctType.SAFETY;
+        } else if (operators.equals("GF")) {
+            return ConjunctType.LIVENESS;
+        } else {
+            return ConjunctType.OTHER;
+        }
+    }
+
+    private static void clearSpecPartFromModule(SMVModule m, ConjunctType t) throws Exception {
+        // For some unknown reason, removeAllIniRestrictions() and removeAllTransRestrictions() don't seem to work
+        if (t == ConjunctType.INITIAL) {
+            m.setInitial(Env.TRUE());
+        } else if (t == ConjunctType.SAFETY) {
+            m.disjunctTrans(Env.TRUE());
+        } else if (t == ConjunctType.LIVENESS) {
+            // Gotta clear these out one by one, apparently
+            while (m.justiceNum() > 0) {
+                m.popLastJustice();
+            }
+        }
+    }
+}

src/examples/unsynth/unsynth_counter.spec

@@ -13,6 +13,9 @@ extinguish, 0
 CompileOptions:
 convexify: True
 parser: structured
+symbolic: False
+use_region_bit_encoding: True
+synthesizer: jtlv
 fastslow: False
 decompose: True
 
@@ -50,9 +53,14 @@ Visit porch
 
 if you are sensing fire then do not living
 if you are sensing person then do not kitchen
+
+#always not living
+#always not kitchen
+
 always not radio
+if you were activating radio then do radio
 
 always not (fire and person)
 
-Always kitchen or porch or deck or bedroom or dining or living
+#Always kitchen or porch or deck or bedroom or dining or living
 

src/examples/unsynth/unsynth_simple.spec

@@ -13,9 +13,11 @@ extinguish, 0
 CompileOptions:
 convexify: True
 parser: structured
+symbolic: False
+use_region_bit_encoding: True
+synthesizer: jtlv
 fastslow: False
 decompose: True
-use_region_bit_encoding: True
 
 Customs: # List of custom propositions
 carrying_item
@@ -51,6 +53,7 @@ Spec: # Specification in structured English
 Env starts with false
 Robot starts in deck
 Always porch
+Always drop
 
 ##Environment safety unsatisfiable -- single step
 #Env starts with false