[feature] issue #15 mostly complete

Implemented a realizes relation between justification diagram and pattern. Still one issue that must be addressed where diagrams are overlapping on each other.
ace-design · Oct 5, 2023 · 144f697 · 144f697
1 parent ff18fbb
commit 144f697
Show file tree

Hide file tree

Showing 9 changed files with 136 additions and 36 deletions.
diff --git a/src/main/java/ca/mcscert/jpipe/compiler/ModelCreationListener.java b/src/main/java/ca/mcscert/jpipe/compiler/ModelCreationListener.java
@@ -3,17 +3,25 @@
 import ca.mcscert.jpipe.compiler.builders.ConcreteJustificationBuilder;
 import ca.mcscert.jpipe.compiler.builders.JustificationBuilder;
 import ca.mcscert.jpipe.compiler.builders.JustificationPatternBuilder;
+import ca.mcscert.jpipe.compiler.builders.ImplementJustificationBuilder;
 import ca.mcscert.jpipe.model.*;
 import ca.mcscert.jpipe.model.justification.*;
 import ca.mcscert.jpipe.syntax.JPipeBaseListener;
 import ca.mcscert.jpipe.syntax.JPipeParser;
+import ca.mcscert.jpipe.compiler.CompilationError;
+
 
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
 
 import java.io.FileNotFoundException;
 import java.nio.file.Paths;
+
+import java.util.HashMap;
+import java.util.Map;
+
 import java.util.ArrayList;
+
 import java.util.List;
 import java.nio.file.Path;
 
@@ -24,7 +32,7 @@ public class ModelCreationListener extends JPipeBaseListener {
     private static Logger logger = LogManager.getLogger(ModelCreationListener.class);
 
     private JustificationBuilder justifBuilder;
-    private final List<JustificationDiagram> justifications = new ArrayList<>();
+    private final Map<String,JustificationDiagram> justifications = new HashMap<>();
 
     private Unit result;
     private Path fileName;
@@ -37,7 +45,7 @@ public ModelCreationListener(String fileName, Compiler compiler) {
     }
 
     public Unit build() {
-        for (JustificationDiagram justification: justifications) {
+        for (JustificationDiagram justification: justifications.values()) {
             result.add(justification);
         }
         return result;
@@ -48,16 +56,31 @@ public Unit build() {
 
     @Override
     public void enterJustification(JPipeParser.JustificationContext ctx) {
-        logger.trace("Entering Justification [" + ctx.id.getText() + "]");
-        justifBuilder = new ConcreteJustificationBuilder(ctx.id.getText());
+        if (ctx.parent!=null){
+            logger.trace("Implementation of [" + ctx.parent.getText() + "]");
+                if (justifications.get(ctx.parent.getText())!=null){
+                    try{
+                        JustificationPattern parent_pattern=(JustificationPattern)justifications.get(ctx.parent.getText());
+                        justifBuilder = new ImplementJustificationBuilder(ctx.id.getText(),parent_pattern);
+                    }catch (ClassCastException e){
+                        logger.trace("Cannot implement [" + ctx.parent.getText() + "] since it is not a pattern");
+                        throw new RuntimeException(e);        
+                    }
+                }else{
+                    throw new CompilationError(ctx.id.getLine(), ctx.id.getStartIndex(), "Pattern does not exist");
+
+                }
+        }else{
+            logger.trace("Entering Justification [" + ctx.id.getText() + "]");
+            justifBuilder = new ConcreteJustificationBuilder(ctx.id.getText());
+        }
         justifBuilder.updateLocation(ctx.getStart().getLine(), ctx.getStart().getCharPositionInLine());
     }
 
     @Override
     public void exitJustification(JPipeParser.JustificationContext ctx) {
         logger.trace("Exiting Justification [" + ctx.id.getText() + "]");
-        JustificationDiagram result = justifBuilder.build();
-        justifications.add(result);
+        justifications.put(ctx.id.getText(),justifBuilder.build());
         justifBuilder = null;
     }
 
@@ -73,8 +96,7 @@ public void enterPattern(JPipeParser.PatternContext ctx) {
     @Override
     public void exitPattern(JPipeParser.PatternContext ctx) {
         logger.trace("Exiting Pattern [" + ctx.id.getText() + "]");
-        JustificationDiagram result = justifBuilder.build();
-        justifications.add(result);
+        justifications.put(ctx.id.getText(),justifBuilder.build());
         justifBuilder = null;
     }
 
@@ -143,15 +165,15 @@ public void enterLoad(JPipeParser.LoadContext ctx) {
         Path loadPath=Paths.get(ctx.file.getText().replace("\"",""));
 
         if (compiler.isCompiled(loadPath)){
-
             logger.trace("  Already entered ["+loadPath.getFileName()+"]");
-
         }else{
             logger.trace("  Entering Load ["+loadPath.getFileName()+"]");
-
             Load loadFile=new Load(loadPath,fileName);
             try {
                 Unit unit = compiler.compile(loadFile.getLoadPath());
+                for (JustificationDiagram j:unit.getJustificationSet()){
+                    justifications.put(j.name(),j);
+                }
                 result.merge(unit);
             } catch (FileNotFoundException e){
                 throw new RuntimeException(e);

diff --git a/src/main/java/ca/mcscert/jpipe/compiler/builders/ConcreteJustificationBuilder.java b/src/main/java/ca/mcscert/jpipe/compiler/builders/ConcreteJustificationBuilder.java
@@ -3,7 +3,7 @@
 import ca.mcscert.jpipe.model.*;
 import ca.mcscert.jpipe.model.justification.*;
 
-public final class ConcreteJustificationBuilder extends JustificationBuilder {
+public class ConcreteJustificationBuilder extends JustificationBuilder {
 
     public ConcreteJustificationBuilder(String name) {
         super(name);

diff --git a/src/main/java/ca/mcscert/jpipe/compiler/builders/ImplementJustificationBuilder.java b/src/main/java/ca/mcscert/jpipe/compiler/builders/ImplementJustificationBuilder.java
@@ -0,0 +1,51 @@
+package ca.mcscert.jpipe.compiler.builders;
+
+import java.util.ArrayList;
+import java.util.List;
+
+import ca.mcscert.jpipe.model.*;
+import ca.mcscert.jpipe.model.justification.*;
+import ca.mcscert.jpipe.model.justification.Conclusion;
+import ca.mcscert.jpipe.model.justification.JustificationElement;
+
+
+public class ImplementJustificationBuilder extends ConcreteJustificationBuilder{
+
+    private final JustificationPattern template;
+
+    public ImplementJustificationBuilder(String name, JustificationPattern template){
+        super(name);
+        this.template=template;
+        extract();
+    }
+
+    private void extract(){
+        this.elements=template.elements();
+        this.dependencies=template.dependencies();
+        this.conclusion=template.conclusion();
+    }
+
+    @Override
+    public void addElement(JustificationElement elem) {
+        String identifier = elem.getIdentifier();
+        this.elements.put(identifier,elem);
+    }
+
+    @Override
+    public void addDependency(String from, String to) {
+        List<String> sources = this.dependencies.getOrDefault(to, new ArrayList<>());
+        sources.add(from);
+        this.dependencies.put(to, sources);
+    }
+
+    @Override
+    public void setConclusion(Conclusion conclusion) {
+        this.conclusion = conclusion;
+    }
+
+
+
+
+
+
+}
diff --git a/src/main/java/ca/mcscert/jpipe/compiler/builders/JustificationBuilder.java b/src/main/java/ca/mcscert/jpipe/compiler/builders/JustificationBuilder.java
@@ -15,8 +15,8 @@
 public abstract class JustificationBuilder {
 
     protected final String name;
-    protected final Map<String, JustificationElement> elements;
-    protected final Map<String, List<String>> dependencies;
+    protected Map<String, JustificationElement> elements;
+    protected Map<String, List<String>> dependencies;
 
     protected Conclusion conclusion = null;
 
@@ -56,6 +56,7 @@ public void addElement(JustificationElement elem) {
         this.elements.put(identifier, elem);
     }
 
+
     public void setConclusion(Conclusion conclusion) {
         if (this.conclusion != null) {
             error("A justification cannot lead to two different conclusions");
@@ -71,6 +72,10 @@ protected final void error(String message) {
         }
     }
 
+    public String getJustificationName(){
+        return this.name;
+    }
+
 
     public abstract JustificationDiagram build();
     public abstract void checkConclusionPredecessor(JustificationElement e);
@@ -86,6 +91,7 @@ protected final void fill(Conclusion c) {
             checkConclusionPredecessor(source);
             Strategy strategy = (Strategy) source;
             c.addSupport(strategy);
+
             fill(strategy);
         }
     }
@@ -114,6 +120,16 @@ protected final void fill(SubConclusion sc) {
         }
     }
 
+    // @Override
+    // public boolean equals(Object o){
+    //     if (o instanceof JustificationBuilder){
+    //         JustificationBuilder comparable = (JustificationBuilder)o;
+    //         return (comparable.getJustificationName().equals(this.name));
+    //     }else{
+    //         return false;
+    //     }
+    // }
+
 
 
 }
diff --git a/src/main/java/ca/mcscert/jpipe/compiler/builders/JustificationPatternBuilder.java b/src/main/java/ca/mcscert/jpipe/compiler/builders/JustificationPatternBuilder.java
@@ -15,7 +15,7 @@ public JustificationPatternBuilder(String name) {
     public JustificationDiagram build() {
         this.line = -1; this.character = -1;
         logger.trace("Finalizing build of Pattern ["+this.name+"]");
-        JustificationDiagram result = new JustificationPattern(this.name, this.conclusion);
+        JustificationDiagram result = new JustificationPattern(this.name, this.conclusion, this.elements,this.dependencies);
         fill(this.conclusion);
         logger.trace("Finalization complete! ["+this.name+"]");
         return result;

diff --git a/src/main/java/ca/mcscert/jpipe/model/justification/JustificationPattern.java b/src/main/java/ca/mcscert/jpipe/model/justification/JustificationPattern.java
@@ -3,11 +3,22 @@
 import ca.mcscert.jpipe.model.JustificationDiagram;
 import ca.mcscert.jpipe.visitors.AbstractVisitor;
 
-public record JustificationPattern(String name, Conclusion conclusion) implements JustificationDiagram {
+import java.util.Map;
+import java.util.List;
+
+public record JustificationPattern(String name, Conclusion conclusion, Map<String, JustificationElement> elements, Map<String,List<String>> dependencies) implements JustificationDiagram {
 
     @Override
     public void accept(AbstractVisitor<?> visitor) {
         visitor.visit(this);
     }
 
+    public Map<String, JustificationElement> elements(){
+        return elements;
+    }
+
+    public Map<String, List<String>> dependencies(){
+        return dependencies;
+    }
+
 }
diff --git a/src/test/resources/pattern_declaration.jd b/src/test/resources/pattern_declaration.jd
@@ -0,0 +1,15 @@
+pattern prover_pattern {
+
+    @support Su1 is "Model is ready"
+    @support Su2 is "Prover is available"
+    evidence Su3 is "Scenario are available"
+
+    strategy St1 is "Prove model"
+    Su1 supports St1
+    Su2 supports St1
+    Su3 supports St1
+
+    conclusion C is "Model is correct"
+    St1 supports C
+
+}
diff --git a/src/test/resources/patterns.jd b/src/test/resources/patterns.jd
@@ -1,23 +1,6 @@
+load "./pattern_declaration.jd"
 
-load "./with_impl.jd"
 
-pattern prover_pattern {
-
-    @support Su1 is "Model is ready"
-    @support Su2 is "Prover is available"
-    evidence Su3 is "Scenario are available"
-
-    strategy St1 is "Prove model"
-    Su1 supports St1
-    Su2 supports St1
-    Su3 supports St1
-
-    conclusion C is "Model is correct"
-    St1 supports C
-
-}
-
-/*
 justification J1 implements prover_pattern {
 
     sub-conclusion Su1 is "Merged model is available"
@@ -28,5 +11,7 @@ justification J1 implements prover_pattern {
 
     evidence Su2 is "TINA is available"
 }
-*/
+
+
+
 
diff --git a/src/test/resources/with_impl.jd b/src/test/resources/with_impl.jd
@@ -1,7 +1,7 @@
 
 load "./patterns.jd"
 
-implementation I1 of prove_model {
+implementation I1 of prover_pattern {
 
     implements Su1 {
       probe is count_files('./models/*.ndr')