From 144f69783bbffb85f57a92d7705af3101ab463ca Mon Sep 17 00:00:00 2001 From: Nirmal-code Date: Thu, 5 Oct 2023 18:46:46 -0400 Subject: [PATCH] [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. --- .../jpipe/compiler/ModelCreationListener.java | 44 ++++++++++++---- .../ConcreteJustificationBuilder.java | 2 +- .../ImplementJustificationBuilder.java | 51 +++++++++++++++++++ .../builders/JustificationBuilder.java | 20 +++++++- .../builders/JustificationPatternBuilder.java | 2 +- .../justification/JustificationPattern.java | 13 ++++- src/test/resources/pattern_declaration.jd | 15 ++++++ src/test/resources/patterns.jd | 23 ++------- src/test/resources/with_impl.jd | 2 +- 9 files changed, 136 insertions(+), 36 deletions(-) create mode 100644 src/main/java/ca/mcscert/jpipe/compiler/builders/ImplementJustificationBuilder.java create mode 100644 src/test/resources/pattern_declaration.jd diff --git a/src/main/java/ca/mcscert/jpipe/compiler/ModelCreationListener.java b/src/main/java/ca/mcscert/jpipe/compiler/ModelCreationListener.java index 9803aa0c..a1d9b5d0 100644 --- 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 justifications = new ArrayList<>(); + private final Map 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 index 8859a2b5..f7659896 100644 --- 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 new file mode 100644 index 00000000..c08d15ae --- /dev/null +++ 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 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 index 02f49aef..0827ecb8 100644 --- 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 elements; - protected final Map> dependencies; + protected Map elements; + protected Map> 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 index 86308b2e..a2fd571a 100644 --- 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 index 8f59c20c..94425206 100644 --- 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 elements, Map> dependencies) implements JustificationDiagram { @Override public void accept(AbstractVisitor visitor) { visitor.visit(this); } + public Map elements(){ + return elements; + } + + public Map> dependencies(){ + return dependencies; + } + } diff --git a/src/test/resources/pattern_declaration.jd b/src/test/resources/pattern_declaration.jd new file mode 100644 index 00000000..3b215a17 --- /dev/null +++ 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 + +} \ No newline at end of file diff --git a/src/test/resources/patterns.jd b/src/test/resources/patterns.jd index b6028cf6..176ea1c1 100644 --- 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 index cc065a4f..274af163 100644 --- 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')