Update

api/src/main/java/pt/haslab/specassistant/data/policy/Binary.java

@@ -27,6 +27,8 @@ public Double apply(Transition transition) {
             case "/" -> left.apply(transition) / right.apply(transition);
             case "+" -> left.apply(transition) + right.apply(transition);
             case "-" -> left.apply(transition) - right.apply(transition);
+            case "max" -> Math.max(left.apply(transition), right.apply(transition));
+            case "min" -> Math.min(left.apply(transition), right.apply(transition));
             default -> throw new UnkownOperationException("Unkown operation " + operator);
         };
     }
@@ -47,6 +49,15 @@ public static Binary sub(PolicyRule left, PolicyRule right) {
         return new Binary("-", left, right);
     }
 
+    public static Binary max(PolicyRule left, PolicyRule right) {
+        return new Binary("max", left, right);
+    }
+
+    public static Binary min(PolicyRule left, PolicyRule right) {
+        return new Binary("min", left, right);
+    }
+
+
     @Override
     public String toString() {
         return "(" + left + " " + operator + " " + right + ")";
@@ -60,4 +71,9 @@ public static PolicyRule scale(Double scalar, PolicyRule p) {
     public static PolicyRule sumOld(PolicyRule p) {
         return new Binary("+", p, Var.old());
     }
+
+    public static PolicyRule oneMinusPrefTimesCost(PolicyRule pref, PolicyRule cost) {
+        return sum(mult(sub(Constant.of(1.0), pref), cost), Var.old());
+    }
+
 }

api/src/main/java/pt/haslab/specassistant/data/policy/PolicyOption.java

@@ -4,7 +4,7 @@
 import lombok.Data;
 import lombok.NoArgsConstructor;
 
-import java.util.List;
+import java.util.Map;
 
 @Data
 @AllArgsConstructor
@@ -26,16 +26,15 @@ public static PolicyOption maxPercentage(PolicyRule r) {
         return new PolicyOption(r, 1.0, Objective.MAX);
     }
 
-    public static final List<PolicyOption> samples = List.of(
-            minimize(PolicyRule.costPrefMix(Var.arrivals(), Var.ted())),
-            minimize(PolicyRule.costPrefMix(Var.arrivals(), Binary.sum(Binary.scale(0.7, Var.ted()), Binary.scale(0.3, Var.complexity())))),
-            minimize(Binary.sumOld(Var.ted())),
-            minimize(Binary.sumOld(Var.complexity())),
-            minimize(Binary.sumOld(Constant.of(1.0))),
-            minimize(Binary.sumOld(Binary.sum(Binary.scale(0.7, Var.ted()), Binary.scale(0.3, Var.complexity())))),
-            maxPercentage(Binary.mult(Var.arrivals(), Var.old())),
-            maxPercentage(Binary.mult(Var.arrivals(), Var.old()))
-
+    public static final Map<String,PolicyOption> samples = Map.of(
+            "TEDxArrival",minimize(Binary.oneMinusPrefTimesCost(Var.arrivals(), Var.ted())),
+            "TEDCOMPxArrival",minimize(Binary.oneMinusPrefTimesCost(Var.arrivals(), Binary.sum(Binary.scale(0.7, Var.ted()), Binary.scale(0.3, Var.complexity())))),
+            "TED",minimize(Binary.sumOld(Var.ted())),
+            "COMP",minimize(Binary.sumOld(Var.complexity())),
+            "ONE",minimize(Binary.sumOld(Constant.of(1.0))),
+            "TEDCOMP",minimize(Binary.sumOld(Binary.sum(Binary.scale(0.7, Var.ted()), Binary.scale(0.3, Var.complexity())))),
+            "Arrival",maxPercentage(Binary.mult(Var.arrivals(), Var.old())),
+            "Departure",maxPercentage(Binary.mult(Var.departures(), Var.old()))
     );
 
 }

api/src/main/java/pt/haslab/specassistant/data/policy/PolicyRule.java

@@ -22,7 +22,4 @@ public abstract class PolicyRule implements Function<Transition, Double> {
 
     public abstract void normalizeByGraph(ObjectId objectId);
 
-    public static PolicyRule costPrefMix(PolicyRule pref, PolicyRule cost) {
-        return Binary.sum(Binary.mult(Binary.sub(Constant.of(1.0), pref), cost), Var.old());
-    }
 }

api/src/main/java/pt/haslab/specassistant/data/policy/Var.java

@@ -32,6 +32,10 @@ public static Var arrivals() {
         return of(Name.ARRIVALS);
     }
 
+    public static Var departures() {
+        return of(Name.DEPARTURES);
+    }
+
     @Override
     public String toString() {
         return var.toString();

api/src/main/java/pt/haslab/specassistant/repositories/EdgeRepository.java

@@ -5,9 +5,9 @@
 import lombok.Synchronized;
 import org.bson.Document;
 import org.bson.types.ObjectId;
+import pt.haslab.specassistant.data.aggregation.Transition;
 import pt.haslab.specassistant.data.models.Edge;
 import pt.haslab.specassistant.data.models.Node;
-import pt.haslab.specassistant.data.aggregation.Transition;
 
 import java.util.Collection;
 import java.util.List;
@@ -44,13 +44,13 @@ public void clearPolicyFromGraph(ObjectId graph_id) {
         update(new Document("$unset", new Document("policy", null))).where("graph_id", graph_id);
     }
 
-    public Stream<Transition> streamTransitionsByDestinationScoreGT(Node destination, Double min) {
+    public Stream<Transition> streamTransitionsByDestinationScoreNull(Node destination, Double min) {
         return StreamSupport.stream(mongoCollection().aggregate(List.of(
                 new Document("$match", new Document("destination", destination.id)),
                 new Document("$replaceRoot", new Document("newRoot", new Document("edge", "$$ROOT"))),
                 new Document("$lookup", new Document("from", "Node").append("localField", "edge.origin").append("foreignField", "_id").append("as", "from")),
                 new Document("$unwind", "$from"),
-                new Document("$match", new Document("$or", List.of(new Document("from.score", new Document("$gt", min)), new Document("from.score", null))))
+                new Document("$match", new Document(new Document("from.score", new Document("$ne", null))))
         ), Transition.class).spliterator(), false).peek(x -> x.setTo(destination));
     }
 

api/src/main/java/pt/haslab/specassistant/repositories/ModelRepository.java

@@ -9,6 +9,7 @@
 
 import java.util.Collection;
 import java.util.List;
+import java.util.stream.Collectors;
 import java.util.stream.Stream;
 import java.util.stream.StreamSupport;
 
@@ -19,6 +20,10 @@ public Stream<Model> streamByDerivationOfAndOriginal(String derivationOf, String
         return find("derivationOf = ?1 and original = ?2", derivationOf, original).stream();
     }
 
+    public Stream<Model> streamByDerivationOfInAndOriginal(Collection< String> derivationOfx, String original) {
+        return find("derivationOf in ?1 and original = ?2", derivationOfx, original).stream();
+    }
+
     public Stream<Model> streamByOriginalAndUnSat(String original_id) {
         return ByOriginalAndUnSat(original_id).stream();
     }

api/src/main/java/pt/haslab/specassistant/services/GraphIngestor.java

@@ -70,30 +70,30 @@ private static boolean testSpecModifications(CompModule original, CompModule tar
         //List<Sig> tSigs = original.getAllSigs().makeConstList();
     }
 
-    private Map<ObjectId, ObjectId> walkModelTreeStep(Predicate<Model> model_filter, Map<String, Challenge> cmdToExercise, Predicate<CompModule> modifiedPred, Model current, Map<ObjectId, ObjectId> context) {
+        private Map<ObjectId, ObjectId> walkModelTreeStep(Predicate<Model> model_filter, Map<String, Challenge> cmdToChallenge, Predicate<CompModule> modifiedPred, Model current, Map<ObjectId, ObjectId> context) {
         try {
-            if (model_filter.test(current) && current.isValidExecution() && cmdToExercise.containsKey(current.getCmd_n())) {
+            if (model_filter.test(current) && current.isValidExecution() && cmdToChallenge.containsKey(current.getCmd_n())) {
 
                 CompModule world = ParseUtil.parseModel(current.getCode());
-                Challenge exercise = cmdToExercise.get(current.getCmd_n());
-                ObjectId contextId = exercise.id;
+                Challenge challenge = cmdToChallenge.get(current.getCmd_n());
+                ObjectId contextId = challenge.id;
                 ObjectId old_node_id = context.get(contextId);
 
                 boolean modified = modifiedPred.test(world);
 
-                if (exercise.isValidCommand(world, current.getCmd_i())) {
+                if (challenge.isValidCommand(world, current.getCmd_i())) {
                     boolean valid = current.getSat() == 0;
 
-                    Map<String, String> formula = Node.getNormalizedFormulaFrom(world.getAllFunc().makeConstList(), exercise.getTargetFunctions());
+                    Map<String, String> formula = Node.getNormalizedFormulaFrom(world.getAllFunc().makeConstList(), challenge.getTargetFunctions());
 
-                    nodeRepo.incrementOrCreate(formula, valid, exercise.getGraph_id(), modified ? current.getId() : null);
-                    ObjectId new_node_id = nodeRepo.findByGraphIdAndFormula(exercise.getGraph_id(), formula).orElseThrow().getId();
+                    nodeRepo.incrementOrCreate(formula, valid, challenge.getGraph_id(), modified ? current.getId() : null);
+                    ObjectId new_node_id = nodeRepo.findByGraphIdAndFormula(challenge.getGraph_id(), formula).orElseThrow().getId();
 
                     if (!old_node_id.equals(new_node_id)) { // No laces
                         nodeRepo.incrementLeaveById(old_node_id);
                         context = new HashMap<>(context); // Make a new context based on the previous one
                         context.put(contextId, new_node_id);
-                        edgeRepo.incrementOrCreate(exercise.getGraph_id(), old_node_id, new_node_id);
+                        edgeRepo.incrementOrCreate(challenge.getGraph_id(), old_node_id, new_node_id);
                     }
                 }
             }
@@ -105,25 +105,25 @@ private Map<ObjectId, ObjectId> walkModelTreeStep(Predicate<Model> model_filter,
         return context;
     }
 
-    public CompletableFuture<Void> walkModelTree(Model root, Predicate<Model> model_filter, Collection<Challenge> exercises) {
-        if (exercises.isEmpty())
+    public CompletableFuture<Void> walkModelTree(Model root, Predicate<Model> model_filter, Collection<Challenge> challenges) {
+        if (challenges.isEmpty())
             return CompletableFuture.completedFuture(null);
 
         CompModule world = ParseUtil.parseModel(root.getCode());
 
-        Map<String, Challenge> cmdToExercise = exercises.stream().collect(Collectors.toUnmodifiableMap(Challenge::getCmd_n, x -> x));
-        Map<ObjectId, ObjectId> exerciseToNodeId = new HashMap<>();
+        Map<String, Challenge> cmdToChallenge = challenges.stream().collect(Collectors.toUnmodifiableMap(Challenge::getCmd_n, x -> x));
+        Map<ObjectId, ObjectId> challengeToNodeId = new HashMap<>();
 
-        cmdToExercise.values().forEach(exercise -> {
-                    Map<String, String> formula = Node.getNormalizedFormulaFrom(world.getAllFunc().makeConstList(), exercise.getTargetFunctions());
-                    nodeRepo.incrementOrCreate(formula, false, exercise.getGraph_id(), null);
-                    exerciseToNodeId.put(exercise.id, nodeRepo.findByGraphIdAndFormula(exercise.getGraph_id(), formula).orElseThrow().getId());
+        cmdToChallenge.values().forEach(challenge -> {
+                    Map<String, String> formula = Node.getNormalizedFormulaFrom(world.getAllFunc().makeConstList(), challenge.getTargetFunctions());
+                    nodeRepo.incrementOrCreate(formula, false, challenge.getGraph_id(), null);
+                    challengeToNodeId.put(challenge.id, nodeRepo.findByGraphIdAndFormula(challenge.getGraph_id(), formula).orElseThrow().getId());
                 }
         );
         return abstractWalkModelTree(
-                (m, ctx) -> walkModelTreeStep(model_filter, cmdToExercise, w -> testSpecModifications(world, w), m, ctx),
+                (m, ctx) -> walkModelTreeStep(model_filter, cmdToChallenge, w -> testSpecModifications(world, w), m, ctx),
                 model -> modelRepo.streamByDerivationOfAndOriginal(model.getId(), model.getOriginal()),
-                exerciseToNodeId,
+                challengeToNodeId,
                 root
         );
     }
@@ -175,17 +175,17 @@ public CompletableFuture<Void> parseModelTree(String model_id, Predicate<Model>
         return parseModelTree(model_id, model_filter, challengeRepo.streamByModelId(model_id).collect(Collectors.toSet()));
     }
 
-    public CompletableFuture<Void> parseModelTree(String model_id, Predicate<Model> model_filter, Collection<Challenge> exercises) {
+    public CompletableFuture<Void> parseModelTree(String model_id, Predicate<Model> model_filter, Collection<Challenge> challenges) {
         Model model = modelRepo.findById(model_id);
 
         CompModule base_world = ParseUtil.parseModel(model.getCode());
 
         AtomicLong parsingTime = new AtomicLong(System.nanoTime());
-        Map<ObjectId, Long> count = exercises.stream().map(Challenge::getGraph_id).collect(Collectors.toMap(x -> x, x -> nodeRepo.getTotalVisitsFromGraph(x)));
+        Map<ObjectId, Long> count = challenges.stream().map(Challenge::getGraph_id).collect(Collectors.toMap(x -> x, x -> nodeRepo.getTotalVisitsFromGraph(x)));
 
-        return walkModelTree(model, model_filter, exercises)
+        return walkModelTree(model, model_filter, challenges)
                 .thenRun(() -> parsingTime.updateAndGet(l -> System.nanoTime() - l))
-                .thenCompose(nil -> FutureUtil.runEachAsync(exercises,
+                .thenCompose(nil -> FutureUtil.runEachAsync(challenges,
                         ex -> {
                             long st = System.nanoTime();
                             AtomicLong local_count = new AtomicLong();

api/src/main/java/pt/haslab/specassistant/services/GraphManager.java

@@ -33,7 +33,7 @@ public class GraphManager {
     @Inject
     EdgeRepository edgeRepo;
     @Inject
-    ChallengeRepository exerciseRepo;
+    ChallengeRepository challengeRepo;
 
     public void cleanGraph(ObjectId graph_id) {
         nodeRepo.deleteByGraphId(graph_id);
@@ -42,51 +42,51 @@ public void cleanGraph(ObjectId graph_id) {
 
     public void deleteGraph(ObjectId graph_id) {
         cleanGraph(graph_id);
-        exerciseRepo.deleteByGraphId(graph_id);
+        challengeRepo.deleteByGraphId(graph_id);
         Graph.deleteById(graph_id);
     }
 
     public void dropEverything() {
         Graph.deleteAll();
         nodeRepo.deleteAll();
         edgeRepo.deleteAll();
-        exerciseRepo.deleteAll();
+        challengeRepo.deleteAll();
     }
 
     public void generateChallenge(ObjectId graph_id, String model_id, Integer secretCommandCount, String cmd_n, Set<String> targetFunctions) {
-        if (exerciseRepo.notExistsModelIdAndCmdN(model_id, cmd_n)) {
-            exerciseRepo.persistOrUpdate(new Challenge(model_id, graph_id, secretCommandCount, cmd_n, targetFunctions));
+        if (challengeRepo.notExistsModelIdAndCmdN(model_id, cmd_n)) {
+            challengeRepo.persistOrUpdate(new Challenge(model_id, graph_id, secretCommandCount, cmd_n, targetFunctions));
         }
     }
 
-    public void generateExercisesWithGraphIdFromSecrets(Function<String, ObjectId> commandToGraphId, String model_id) {
+    public void generateChallengesWithGraphIdFromSecrets(Function<String, ObjectId> commandToGraphId, String model_id) {
         Model m = modelRepo.findByIdOptional(model_id).orElseThrow();
         CompModule world = ParseUtil.parseModel(m.getCode());
         List<Pos> secretPositions = secretPos(world.path, m.getCode());
 
         Map<String, Set<String>> targets = AlloyUtil.getFunctionWithPositions(world, secretPositions);
         Integer cmdCount = targets.size();
 
-        exerciseRepo.persistOrUpdate(targets.entrySet().stream().map(x -> new Challenge(model_id, commandToGraphId.apply(x.getKey()), cmdCount, x.getKey(), x.getValue())));
+        challengeRepo.persistOrUpdate(targets.entrySet().stream().map(x -> new Challenge(model_id, commandToGraphId.apply(x.getKey()), cmdCount, x.getKey(), x.getValue())));
     }
 
     public Set<ObjectId> getModelGraphs(String modelid) {
-        return exerciseRepo.streamByModelId(modelid).map(Challenge::getGraph_id).collect(Collectors.toSet());
+        return challengeRepo.streamByModelId(modelid).map(Challenge::getGraph_id).collect(Collectors.toSet());
     }
 
     public void deleteAllGraphStructures() {
         nodeRepo.deleteAll();
         edgeRepo.deleteAll();
     }
 
-    public void deleteExerciseByModelIDs(List<String> ids, boolean cascadeToGraphs) {
+    public void deleteChallengesByModelIDs(List<String> ids, boolean cascadeToGraphs) {
         if (!cascadeToGraphs) {
-            exerciseRepo.deleteByModelIdIn(ids);
+            challengeRepo.deleteByModelIdIn(ids);
         } else {
-            Set<ObjectId> graph_ids = exerciseRepo.streamByModelIdIn(ids).map(Challenge::getGraph_id).collect(Collectors.toSet());
-            exerciseRepo.deleteByModelIdIn(ids);
+            Set<ObjectId> graph_ids = challengeRepo.streamByModelIdIn(ids).map(Challenge::getGraph_id).collect(Collectors.toSet());
+            challengeRepo.deleteByModelIdIn(ids);
             graph_ids.forEach(graph_id -> {
-                if (!exerciseRepo.containsGraph(graph_id))
+                if (!challengeRepo.containsGraph(graph_id))
                     deleteGraph(graph_id);
             });
         }