diff --git a/de.prob.core/src/de/prob/animator/domainobjects/EBEvent.java b/de.prob.core/src/de/prob/animator/domainobjects/EBEvent.java new file mode 100644 index 0000000000000000000000000000000000000000..61a159caaff667c5532c2f8f2f35512a6e70ebc7 --- /dev/null +++ b/de.prob.core/src/de/prob/animator/domainobjects/EBEvent.java @@ -0,0 +1,47 @@ +package de.prob.animator.domainobjects; + +import java.util.Arrays; + +import de.prob.model.eventb.EventB; +import de.prob.model.representation.IEntity; +import de.prob.model.representation.Label; + +public class EBEvent extends Label { + + final public Label refines = new Label("REFINES"); + final public Label parameters = new Label("ANY"); + final public Label guards = new Label("WHERE"); + final public Label witnesses = new Label("WITH"); + final public Label actions = new Label("THEN"); + + public EBEvent(final String name) { + super(name); + children.addAll(Arrays.asList(new IEntity[] { refines, parameters, + guards, witnesses, actions })); + } + + @Override + public String toString() { + return name; + } + + public void addRefinement(final String refinementName) { + refines.addChild(new Label(refinementName)); + } + + public void addParameter(final String parameter) { + parameters.addChild(new EventB(parameter)); + } + + public void addGuard(final String guard) { + guards.addChild(new EventB(guard)); + } + + public void addWitness(final String witness) { + witnesses.addChild(new EventB(witness)); + } + + public void addAction(final String action) { + actions.addChild(new Label(action)); + } +} diff --git a/de.prob.core/src/de/prob/animator/domainobjects/EvalElementType.java b/de.prob.core/src/de/prob/animator/domainobjects/EvalElementType.java new file mode 100644 index 0000000000000000000000000000000000000000..95ff5f1c565a45e6fb653173cec26c0fce64c756 --- /dev/null +++ b/de.prob.core/src/de/prob/animator/domainobjects/EvalElementType.java @@ -0,0 +1,11 @@ +package de.prob.animator.domainobjects; + +public enum EvalElementType { + PREDICATE, EXPRESSION; + + @Override + public String toString() { + return "#" + super.toString(); + } + +} diff --git a/de.prob.core/src/de/prob/animator/domainobjects/IEvalElement.java b/de.prob.core/src/de/prob/animator/domainobjects/IEvalElement.java new file mode 100644 index 0000000000000000000000000000000000000000..e6fd3f173ba64ae683f5e37d33ced493d3969fb7 --- /dev/null +++ b/de.prob.core/src/de/prob/animator/domainobjects/IEvalElement.java @@ -0,0 +1,11 @@ +package de.prob.animator.domainobjects; + +import de.prob.prolog.output.IPrologTermOutput; + +public interface IEvalElement { + public abstract String getCode(); + + public abstract void printProlog(IPrologTermOutput pout); + + public abstract String getKind(); +} diff --git a/de.prob.core/src/de/prob/model/eventb/EBContext.java b/de.prob.core/src/de/prob/model/eventb/EBContext.java new file mode 100644 index 0000000000000000000000000000000000000000..0d6a1ae9605f451412f5f20049db58e3c1d20461 --- /dev/null +++ b/de.prob.core/src/de/prob/model/eventb/EBContext.java @@ -0,0 +1,33 @@ +package de.prob.model.eventb; + +import java.util.Arrays; + +import de.prob.model.representation.IEntity; +import de.prob.model.representation.Label; + +public class EBContext extends Label { + + public Label sets = new Label("Sets"); + public Label constants = new Label("Constants"); + public Label axioms = new Label("Axioms"); + + public EBContext(final String name) { + super(name); + + children.addAll(Arrays + .asList(new IEntity[] { sets, constants, axioms })); + } + + public void addSet(final String set) { + sets.addChild(new EventB(set)); + } + + public void addConstant(final String constant) { + constants.addChild(new EventB(constant)); + } + + public void addAxiom(final String axiom) { + axioms.addChild(new EventB(axiom)); + } + +} diff --git a/de.prob.core/src/de/prob/model/eventb/EBMachine.java b/de.prob.core/src/de/prob/model/eventb/EBMachine.java new file mode 100644 index 0000000000000000000000000000000000000000..b837625671e974b25017917f22f0c4ec794e39b8 --- /dev/null +++ b/de.prob.core/src/de/prob/model/eventb/EBMachine.java @@ -0,0 +1,37 @@ +package de.prob.model.eventb; + +import java.util.Arrays; + +import de.prob.animator.domainobjects.EBEvent; +import de.prob.model.representation.IEntity; +import de.prob.model.representation.Label; + +public class EBMachine extends Label { + + final public Label variables = new Label("Variables"); + final public Label invariants = new Label("Invariants"); + final public Label variant = new Label("Variant"); + final public Label events = new Label("Events"); + + public EBMachine(final String name) { + super(name); + children.addAll(Arrays.asList(new IEntity[] { variables, invariants, + variant, events })); + } + + public void addVariable(final String variable) { + variables.addChild(new EventB(variable)); + } + + public void addInvariant(final String invariant) { + invariants.addChild(new EventB(invariant)); + } + + public void addVariant(final String variant) { + this.variant.addChild(new EventB(variant)); + } + + public void addEvent(final String event) { + events.addChild(new EBEvent(event)); + } +} diff --git a/de.prob.core/src/de/prob/model/eventb/EventB.java b/de.prob.core/src/de/prob/model/eventb/EventB.java new file mode 100644 index 0000000000000000000000000000000000000000..5c6c3b9d1353e1fa19d67e9c81373579c988dbd8 --- /dev/null +++ b/de.prob.core/src/de/prob/model/eventb/EventB.java @@ -0,0 +1,121 @@ +package de.prob.model.eventb; + +import static de.prob.animator.domainobjects.EvalElementType.EXPRESSION; +import static de.prob.animator.domainobjects.EvalElementType.PREDICATE; + +import java.util.ArrayList; +import java.util.LinkedList; +import java.util.List; + +import org.eventb.core.ast.ASTProblem; +import org.eventb.core.ast.Expression; +import org.eventb.core.ast.FormulaFactory; +import org.eventb.core.ast.IParseResult; +import org.eventb.core.ast.LanguageVersion; +import org.eventb.core.ast.Predicate; + +import de.prob.animator.domainobjects.IEvalElement; +import de.prob.eventb.translator.ExpressionVisitor; +import de.prob.eventb.translator.PredicateVisitor; +import de.be4.classicalb.core.parser.analysis.prolog.ASTProlog; +import de.be4.classicalb.core.parser.node.Node; +import de.prob.model.representation.FormulaUUID; +import de.prob.model.representation.IEntity; +import de.prob.prolog.output.IPrologTermOutput; +import de.prob.unicode.UnicodeTranslator; + +public class EventB implements IEvalElement, IEntity { + + public FormulaUUID uuid = new FormulaUUID(); + + private final String code; + private String kind; + private Node ast = null; + + public EventB(final String code) { + this.code = code; + } + + private void ensureParsed() { + final String unicode = UnicodeTranslator.toUnicode(code); + kind = PREDICATE.toString(); + IParseResult parseResult = FormulaFactory.getDefault().parsePredicate( + unicode, LanguageVersion.LATEST, null); + + if (!parseResult.hasProblem()) { + ast = preparePredicateAst(parseResult); + + } else { + kind = EXPRESSION.toString(); + parseResult = FormulaFactory.getDefault().parseExpression(unicode, + LanguageVersion.LATEST, null); + ast = prepareExpressionAst(parseResult); + } + if (parseResult.hasProblem()) { + throwException(code, parseResult); + } + } + + private Node prepareExpressionAst(final IParseResult parseResult) { + final Expression expr = parseResult.getParsedExpression(); + final ExpressionVisitor visitor = new ExpressionVisitor( + new LinkedList<String>()); + expr.accept(visitor); + final Node expression = visitor.getExpression(); + return expression; + } + + private Node preparePredicateAst(final IParseResult parseResult) { + final Predicate parsedPredicate = parseResult.getParsedPredicate(); + final PredicateVisitor visitor = new PredicateVisitor(); + parsedPredicate.accept(visitor); + return visitor.getPredicate(); + } + + private void throwException(final String code, + final IParseResult parseResult) { + final List<ASTProblem> problems = parseResult.getProblems(); + final ArrayList<String> msgs = new ArrayList<String>(); + for (final ASTProblem astProblem : problems) { + msgs.add(astProblem.getMessage().toString()); + } + StringBuilder sb = new StringBuilder(); + for (String string : msgs) { + sb.append(string+"\n"); + } + final String error = sb.toString(); + throw new RuntimeException("Cannot parse " + code + ":\n " + error); // FIXME + } + + @Override + public String getCode() { + return code; + } + + @Override + public void printProlog(final IPrologTermOutput pout) { + if (ast == null) { + ensureParsed(); + } + + assert ast != null; + final ASTProlog prolog = new ASTProlog(pout, null); + ast.apply(prolog); + } + + @Override + public String getKind() { + return kind; + } + + @Override + public List<IEntity> getChildren() { + return new ArrayList<IEntity>(); + } + + @Override + public boolean hasChildren() { + return false; + } + +} diff --git a/de.prob.core/src/de/prob/model/eventb/Model.java b/de.prob.core/src/de/prob/model/eventb/Model.java new file mode 100644 index 0000000000000000000000000000000000000000..5fe40c4878a1875953c381cba1c6c4f79ee29451 --- /dev/null +++ b/de.prob.core/src/de/prob/model/eventb/Model.java @@ -0,0 +1,9 @@ +package de.prob.model.eventb; + +import java.util.ArrayList; +import java.util.List; + +public class Model { + + public List<Relationship> relationships = new ArrayList<Relationship>(); +} diff --git a/de.prob.core/src/de/prob/model/eventb/Relationship.java b/de.prob.core/src/de/prob/model/eventb/Relationship.java new file mode 100644 index 0000000000000000000000000000000000000000..d6b3f130aee5248d1ae72afb65c2d3250c9fef15 --- /dev/null +++ b/de.prob.core/src/de/prob/model/eventb/Relationship.java @@ -0,0 +1,13 @@ +package de.prob.model.eventb; + +import de.prob.model.representation.Label; + +public class Relationship { + public final Label from; + public final Label to; + + public Relationship(Label from,Label to) { + this.from = from; + this.to = to; + } +} diff --git a/de.prob.core/src/de/prob/model/representation/FormulaUUID.java b/de.prob.core/src/de/prob/model/representation/FormulaUUID.java new file mode 100644 index 0000000000000000000000000000000000000000..d84d6c7f28c2e427f674ea6a367dda9f9beb7056 --- /dev/null +++ b/de.prob.core/src/de/prob/model/representation/FormulaUUID.java @@ -0,0 +1,6 @@ +package de.prob.model.representation; + +public class FormulaUUID { + static int count = 0; + public final String uuid = "Formula_" + (++count); +} diff --git a/de.prob.core/src/de/prob/model/representation/IEntity.java b/de.prob.core/src/de/prob/model/representation/IEntity.java new file mode 100644 index 0000000000000000000000000000000000000000..3510e37438070920160fdbb9b10f6be26f898edc --- /dev/null +++ b/de.prob.core/src/de/prob/model/representation/IEntity.java @@ -0,0 +1,9 @@ +package de.prob.model.representation; + +import java.util.List; + +public interface IEntity { + public List<IEntity> getChildren(); + + public boolean hasChildren(); +} diff --git a/de.prob.core/src/de/prob/model/representation/Label.java b/de.prob.core/src/de/prob/model/representation/Label.java new file mode 100644 index 0000000000000000000000000000000000000000..88cb1ed729d911c29346db006d7bef0fc132433c --- /dev/null +++ b/de.prob.core/src/de/prob/model/representation/Label.java @@ -0,0 +1,48 @@ +package de.prob.model.representation; + +import java.util.ArrayList; +import java.util.Collections; +import java.util.List; + +public class Label implements IEntity { + + public List<IEntity> children = new ArrayList<IEntity>(); + protected String name; + private boolean locked = false; + + public Label(final String name) { + this.name = name; + } + + public void addChild(final IEntity child) { + if (!locked) { + children.add(child); + } + } + + @Override + public List<IEntity> getChildren() { + if (locked) { + return Collections.unmodifiableList(children); + } + return children; + } + + public String getName() { + return name; + } + + public void lock() { + locked = true; + for (final IEntity child : children) { + if (child instanceof Label) { + ((Label) child).lock(); + } + } + } + + @Override + public boolean hasChildren() { + return !children.isEmpty(); + } +}