be more generous on what crossrefs are possible.

lip6 · Jul 4, 2024 · dd4af97 · dd4af97
1 parent b10a6e9
commit dd4af97
Showing 1 changed file with 27 additions and 3 deletions.
diff --git a/mist/fr.lip6.mist/src/fr/lip6/mist/io/properties/PropertiesImporter.java b/mist/fr.lip6.mist/src/fr/lip6/mist/io/properties/PropertiesImporter.java
@@ -47,11 +47,18 @@ public void syntaxError(Recognizer<?, ?> recognizer, Object offendingSymbol, int
 	}
 
 
-	class PropertiesVisitor extends PropertiesBaseVisitor<Expression> {
+	private static class PropertiesVisitor extends PropertiesBaseVisitor<Expression> {
 
 		private List<Property> list;
 		private Map<String,Expression> atoms = new HashMap<>();
+		private Map<String,Property> propMap = new HashMap<>();
+
 		private Map<String, Integer> variables;
+
+		private static enum ContextType {
+			CTL, LTL, BOUNDS, INVARIANT
+		}
+		private ContextType context;
 
 		public PropertiesVisitor(List<Property> list, Map<String, Integer> vars) {
 			this.list = list;
@@ -73,12 +80,14 @@ public Expression visitProperties(PropertiesContext ctx) {
 				LogicPropContext logic = prop.logicProp();
 				if (logic.boundsProp() != null) {
 					type = PropertyType.BOUNDS;
+					context = ContextType.BOUNDS;
 					expr = logic.boundsProp().target.accept(this);
                 } else {
                 	BoolPropContext boolProp = logic.boolProp();
 
                 	if (boolProp.reachableProp() != null) {
                 		type = PropertyType.INVARIANT;
+                		context = ContextType.INVARIANT;
                 		ReachablePropContext rp = boolProp.reachableProp();
 						if ("EF".equals(rp.op.getText())) {
 							expr = Expression.nop(Op.EF, rp.predicate.accept(this));
@@ -87,12 +96,15 @@ public Expression visitProperties(PropertiesContext ctx) {
 						}
                 	} else if (boolProp.ctlProp() != null) {
                 		type = PropertyType.CTL;
+                		context = ContextType.CTL;
                 		expr = boolProp.ctlProp().predicate.accept(this);
                 	} else if (boolProp.ltlProp() != null) {
                 		type = PropertyType.LTL;
+                		context = ContextType.LTL;
                 		expr = boolProp.ltlProp().predicate.accept(this);
                 	} else if (boolProp.atomicProp() != null) {
-                		// special case                			
+                		// special case
+                		context = ContextType.INVARIANT;
                 		expr = boolProp.atomicProp().predicate.accept(this);
                 		atoms.put(name, expr);
                 		// next property
@@ -104,6 +116,7 @@ public Expression visitProperties(PropertiesContext ctx) {
 
 				Property newprop = new Property(expr, type, name);				
 				list.add(newprop);
+				propMap.put(name, newprop);
 			}
 			return super.visitProperties(ctx);
 		}
@@ -166,7 +179,18 @@ public Expression visitAtomReference(AtomReferenceContext ctx) {
 			String name = ctx.name.getText();
 			Expression expr = atoms.get(name);
 			if (expr == null) {
-				throw new IllegalArgumentException("Unknown atomic property " + name);
+				Property refd = propMap.get(name);
+				if (refd != null) {
+					if (refd.getType() == PropertyType.LTL && context == ContextType.LTL) {
+						return refd.getBody();
+					} else if ( (refd.getType() == PropertyType.CTL || refd.getType() == PropertyType.INVARIANT) && context == ContextType.CTL) {
+						return refd.getBody();
+					} else {
+						throw new IllegalArgumentException("Cannot refer to property "+ name+ " with type " + refd.getType() + " from the context of " + context);
+					}
+				} else {
+					throw new IllegalArgumentException("Unknown property reference @" + name);
+				}
 			} else {
 				return expr;
 			}