diff --git a/de.prob.core/META-INF/MANIFEST.MF b/de.prob.core/META-INF/MANIFEST.MF
index 183aec64ab8396a38371833010f46f9c636a3346..b58a587fe9433899a58102254213d8cc92978586 100644
--- a/de.prob.core/META-INF/MANIFEST.MF
+++ b/de.prob.core/META-INF/MANIFEST.MF
@@ -59,7 +59,6 @@ Export-Package: com.thoughtworks.xstream,
de.be4.ltl.core.parser.node,
de.be4.ltl.core.parser.parser,
de.hhu.stups.sablecc.patch,
- de.prob.animator.domainobjects,
de.prob.cli,
de.prob.cli.clipatterns,
de.prob.core,
@@ -83,9 +82,6 @@ Export-Package: com.thoughtworks.xstream,
de.prob.eventb.translator.internal,
de.prob.exceptions,
de.prob.logging,
- de.prob.model.eventb,
- de.prob.model.representation,
- de.prob.model.serialize,
de.prob.parser,
de.prob.parserbase,
de.prob.prolog.match,
diff --git a/de.prob.core/src/de/prob/animator/domainobjects/EvalElementType.java b/de.prob.core/src/de/prob/animator/domainobjects/EvalElementType.java
deleted file mode 100644
index 95ff5f1c565a45e6fb653173cec26c0fce64c756..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/animator/domainobjects/EvalElementType.java
+++ /dev/null
@@ -1,11 +0,0 @@
-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/EvaluationResult.java b/de.prob.core/src/de/prob/animator/domainobjects/EvaluationResult.java
deleted file mode 100644
index fb5ce98a7c77defd6ad8ee03b1b86cad06c52d25..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/animator/domainobjects/EvaluationResult.java
+++ /dev/null
@@ -1,102 +0,0 @@
-package de.prob.animator.domainobjects;
-
-import java.util.Arrays;
-import java.util.List;
-
-/**
- * This is what is saved when a formula ({@link IEvalElement}) is executed in
- * the StateSpace
- *
- * @author joy
- *
- */
-public class EvaluationResult {
-
- public final String value;
- public final String solution;
- public final String errors;
- public final String code;
- public final String explanation;
- private final String resultType;
- private final List<String> quantifiedVars;
- private final boolean enumerationWarnings;
- private final String stateid;
-
- public EvaluationResult(final String stateid, final String code,
- final String value, final String solution, final String errors,
- final String resultType, final List<String> quantifiedVars,
- final boolean enumerationWarnings) {
- this.stateid = stateid;
- this.code = code;
- this.value = value;
- this.solution = solution;
- this.errors = errors;
- this.resultType = resultType;
- this.quantifiedVars = quantifiedVars;
- this.enumerationWarnings = enumerationWarnings;
- if (!solutionMode(resultType) && "TRUE".equals(value)) {
- this.explanation = "Solution";
- } else {
- this.explanation = solutionMode(resultType) ? " Solution: "
- : " Counterexample: ";
- }
- }
-
- public EvaluationResult(final String stateid, final String code,
- final String value, final String solution, final String errors,
- final String resultType, final String[] strings,
- final boolean enumerationWarnings) {
- this(stateid, code, value, solution, errors, resultType, Arrays
- .asList(strings), enumerationWarnings);
- }
-
- private boolean solutionMode(final String arg0) {
- return "exists".equals(arg0);
- }
-
- public String getResultType() {
- return resultType;
- }
-
- public List<String> getQuantifiedVars() {
- return quantifiedVars;
- }
-
- public boolean hasEnumerationWarnings() {
- return enumerationWarnings;
- }
-
- public boolean hasError() {
- return errors != null && !errors.isEmpty(); // You're kidding, aren't
- // you? ;-)
- }
-
- public String getErrors() {
- return errors;
- }
-
- public String getValue() {
- return value;
- }
-
- @Override
- public String toString() {
- final String result;
- if (hasError()) {
- result = "'Errors: " + errors + "'";
- } else {
- result = (solution == null || solution.equals("")) ? value : value
- + explanation + solution;
- }
- return result;
- }
-
- public String getStateId() {
- return stateid;
- }
-
- public String getStateid() {
- return stateid;
- }
-
-}
diff --git a/de.prob.core/src/de/prob/animator/domainobjects/EventB.java b/de.prob.core/src/de/prob/animator/domainobjects/EventB.java
deleted file mode 100644
index 15e683a4955385a05cdf4fc2a588702e929c8da4..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/animator/domainobjects/EventB.java
+++ /dev/null
@@ -1,114 +0,0 @@
-package de.prob.animator.domainobjects;
-
-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.prolog.output.IPrologTermOutput;
-import de.prob.unicode.UnicodeTranslator;
-
-/**
- * Representation of an Event-B formula
- *
- * @author joy
- *
- */
-public class EventB implements IEvalElement {
-
- public FormulaUUID uuid = new FormulaUUID();
-
- private final String code;
- private String kind;
- private Node ast = null;
-
- /**
- * @param code
- * - The String which is a representation of the desired Event-B
- * formula
- */
- public EventB(final String code) {
- this.code = UnicodeTranslator.toAscii(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());
- // }
- // final String error = Joiner.on(", \n").join(msgs);
- // throw new EvaluationException("Cannot parse " + code + ":\n " + error);
- // }
-
- @Override
- public String getCode() {
- return code;
- }
-
- @Override
- public boolean equals(final Object that) {
- if (that instanceof EventB) {
- return ((EventB) that).getCode().equals(this.getCode());
- }
- return false;
- }
-
- @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 String toString() {
- return getCode();
- }
-
-}
diff --git a/de.prob.core/src/de/prob/animator/domainobjects/IEvalElement.java b/de.prob.core/src/de/prob/animator/domainobjects/IEvalElement.java
deleted file mode 100644
index e6fd3f173ba64ae683f5e37d33ced493d3969fb7..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/animator/domainobjects/IEvalElement.java
+++ /dev/null
@@ -1,11 +0,0 @@
-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/Context.java b/de.prob.core/src/de/prob/model/eventb/Context.java
deleted file mode 100644
index a978d6d5f5bb6709811241b7edecc5ccc6078a0a..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/model/eventb/Context.java
+++ /dev/null
@@ -1,41 +0,0 @@
-package de.prob.model.eventb;
-
-import java.util.List;
-
-import de.prob.model.representation.AbstractElement;
-import de.prob.model.representation.Axiom;
-import de.prob.model.representation.BSet;
-import de.prob.model.representation.Constant;
-public class Context extends AbstractElement {
-
- private final String name;
-
- public Context(final String name) {
- this.name = name;
- }
-
- public String getName() {
- return name;
- }
-
- public void addExtends(final List<Context> contexts) {
- put(Context.class, contexts);
- }
-
- public void addSets(final List<BSet> sets) {
- put(BSet.class, sets);
- }
-
- public void addConstants(final List<EventBConstant> constants) {
- put(Constant.class, constants);
- }
-
- public void addAxioms(final List<EventBAxiom> axioms) {
- put(Axiom.class, axioms);
- }
-
- @Override
- public String toString() {
- return name;
- }
-}
diff --git a/de.prob.core/src/de/prob/model/eventb/Event.java b/de.prob.core/src/de/prob/model/eventb/Event.java
deleted file mode 100644
index e9071fa4c1f7362e3b20f21ec32b5b8d483a1bf4..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/model/eventb/Event.java
+++ /dev/null
@@ -1,75 +0,0 @@
-package de.prob.model.eventb;
-
-import java.util.List;
-import java.util.Set;
-
-import de.prob.model.representation.AbstractElement;
-import de.prob.model.representation.Action;
-import de.prob.model.representation.BEvent;
-import de.prob.model.representation.Guard;
-
-public class Event extends BEvent {
-
- private final EventType type;
-
- public enum EventType {
- ORDINARY, CONVERGENT, ANTICIPATED
- }
-
- public Event(final String name, final EventType type) {
- super(name);
- this.type = type;
- }
-
- public void addRefines(final List<Event> refines) {
- put(Event.class, refines);
- }
-
- public void addGuards(final List<EventBGuard> guards) {
- put(Guard.class, guards);
- }
-
- public void addActions(final List<EventBAction> actions) {
- put(Action.class, actions);
- }
-
- public void addWitness(final List<Witness> witness) {
- put(Witness.class, witness);
- }
-
- public void addParameters(final List<EventParameter> parameters) {
- put(EventParameter.class, parameters);
- }
-
- public EventType getType() {
- return type;
- }
-
- @Override
- public String toString() {
- return getName();
- }
-
- public String print() {
- StringBuilder sb = new StringBuilder();
- sb.append("Name: " + getName() + "\n");
- sb.append("Type: " + type.toString() + "\n");
- addChildren("Refines", getChildrenOfType(Event.class), sb);
- addChildren("Any", getChildrenOfType(EventParameter.class), sb);
- addChildren("Where", getChildrenOfType(Guard.class), sb);
- addChildren("With", getChildrenOfType(Witness.class), sb);
- addChildren("Then", getChildrenOfType(Action.class), sb);
- return sb.toString();
- }
-
- private void addChildren(final String name,
- final Set<? extends AbstractElement> childrenOfType,
- final StringBuilder sb) {
- if (!childrenOfType.isEmpty()) {
- sb.append(name + ": \n");
- for (AbstractElement abstractElement : childrenOfType) {
- sb.append("\t" + abstractElement.toString() + "\n");
- }
- }
- }
-}
diff --git a/de.prob.core/src/de/prob/model/eventb/EventBAction.java b/de.prob.core/src/de/prob/model/eventb/EventBAction.java
deleted file mode 100644
index 495a3306f026322ed66be61397898b69a80b8d47..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/model/eventb/EventBAction.java
+++ /dev/null
@@ -1,22 +0,0 @@
-package de.prob.model.eventb;
-
-import de.prob.model.representation.Action;
-
-public class EventBAction extends Action {
-
- private final String name;
-
- public EventBAction(final String name, final String code) {
- super(code);
- this.name = name;
- }
-
- public String getName() {
- return name;
- }
-
- @Override
- public String toString() {
- return name + ": " + getCode();
- }
-}
diff --git a/de.prob.core/src/de/prob/model/eventb/EventBAxiom.java b/de.prob.core/src/de/prob/model/eventb/EventBAxiom.java
deleted file mode 100644
index a21374bf45edd9b092e3397ca8f89e395a6d345b..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/model/eventb/EventBAxiom.java
+++ /dev/null
@@ -1,25 +0,0 @@
-package de.prob.model.eventb;
-
-import de.prob.animator.domainobjects.EventB;
-import de.prob.model.representation.Axiom;
-
-public class EventBAxiom extends Axiom {
-
- private final String name;
- private final boolean theorem;
-
- public EventBAxiom(final String name, final String code,
- final boolean theorem) {
- super(new EventB(code));
- this.name = name;
- this.theorem = theorem;
- }
-
- public String getName() {
- return name;
- }
-
- public boolean isTheorem() {
- return theorem;
- }
-}
diff --git a/de.prob.core/src/de/prob/model/eventb/EventBConstant.java b/de.prob.core/src/de/prob/model/eventb/EventBConstant.java
deleted file mode 100644
index 935847691c782219755fcb792ae6aeb8e5732f66..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/model/eventb/EventBConstant.java
+++ /dev/null
@@ -1,18 +0,0 @@
-package de.prob.model.eventb;
-
-import de.prob.animator.domainobjects.EventB;
-import de.prob.model.representation.Constant;
-
-public class EventBConstant extends Constant {
-
- private final String name;
-
- public EventBConstant(final String name) {
- super(new EventB(name));
- this.name = name;
- }
-
- public String getName() {
- return name;
- }
-}
diff --git a/de.prob.core/src/de/prob/model/eventb/EventBGuard.java b/de.prob.core/src/de/prob/model/eventb/EventBGuard.java
deleted file mode 100644
index 2e2bc569062f52170a32eef5e5eba9ad2428f372..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/model/eventb/EventBGuard.java
+++ /dev/null
@@ -1,25 +0,0 @@
-package de.prob.model.eventb;
-
-import de.prob.animator.domainobjects.EventB;
-import de.prob.model.representation.Guard;
-
-public class EventBGuard extends Guard {
-
- private final String name;
- private final boolean theorem;
-
- public EventBGuard(final String name, final String code,
- final boolean theorem) {
- super(new EventB(code));
- this.name = name;
- this.theorem = theorem;
- }
-
- public String getName() {
- return name;
- }
-
- public boolean isTheorem() {
- return theorem;
- }
-}
diff --git a/de.prob.core/src/de/prob/model/eventb/EventBInvariant.java b/de.prob.core/src/de/prob/model/eventb/EventBInvariant.java
deleted file mode 100644
index a49c05d459fc7cb23a014704b4600d0158518713..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/model/eventb/EventBInvariant.java
+++ /dev/null
@@ -1,25 +0,0 @@
-package de.prob.model.eventb;
-
-import de.prob.animator.domainobjects.EventB;
-import de.prob.model.representation.Invariant;
-
-public class EventBInvariant extends Invariant {
-
- private final String name;
- private final boolean theorem;
-
- public EventBInvariant(final String name, final String code,
- final boolean theorem) {
- super(new EventB(code));
- this.name = name;
- this.theorem = theorem;
- }
-
- public String getName() {
- return name;
- }
-
- public boolean isTheorem() {
- return theorem;
- }
-}
diff --git a/de.prob.core/src/de/prob/model/eventb/EventBMachine.java b/de.prob.core/src/de/prob/model/eventb/EventBMachine.java
deleted file mode 100644
index 5998cc8b87e4842b44004ab4165825e7fe427ae8..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/model/eventb/EventBMachine.java
+++ /dev/null
@@ -1,38 +0,0 @@
-package de.prob.model.eventb;
-
-import java.util.List;
-
-import de.prob.model.representation.BEvent;
-import de.prob.model.representation.Invariant;
-import de.prob.model.representation.Machine;
-import de.prob.model.representation.Variable;
-
-public class EventBMachine extends Machine {
- public EventBMachine(final String name) {
- super(name);
- }
-
- public void addRefines(final List<EventBMachine> refines) {
- put(Machine.class, refines);
- }
-
- public void addSees(final List<Context> sees) {
- put(Context.class, sees);
- }
-
- public void addVariables(final List<EventBVariable> variables) {
- put(Variable.class, variables);
- }
-
- public void addInvariants(final List<EventBInvariant> invariants) {
- put(Invariant.class, invariants);
- }
-
- public void addVariant(final List<Variant> variant) {
- put(Variant.class, variant);
- }
-
- public void addEvents(final List<Event> events) {
- put(BEvent.class, events);
- }
-}
diff --git a/de.prob.core/src/de/prob/model/eventb/EventBVariable.java b/de.prob.core/src/de/prob/model/eventb/EventBVariable.java
deleted file mode 100644
index 4ecf1af228d618822d89ee9840f3ecff16368ad6..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/model/eventb/EventBVariable.java
+++ /dev/null
@@ -1,18 +0,0 @@
-package de.prob.model.eventb;
-
-import de.prob.animator.domainobjects.EventB;
-import de.prob.model.representation.Variable;
-
-public class EventBVariable extends Variable {
-
- private final String name;
-
- public EventBVariable(final String name) {
- super(new EventB(name));
- this.name = name;
- }
-
- public String getName() {
- return name;
- }
-}
diff --git a/de.prob.core/src/de/prob/model/eventb/EventParameter.java b/de.prob.core/src/de/prob/model/eventb/EventParameter.java
deleted file mode 100644
index 5ebff9f27bcf3a4c73185beeb9770c59aa6846c9..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/model/eventb/EventParameter.java
+++ /dev/null
@@ -1,22 +0,0 @@
-package de.prob.model.eventb;
-
-import de.prob.model.representation.AbstractElement;
-
-public class EventParameter extends AbstractElement {
-
- private final String name;
-
- public EventParameter(final String name) {
- this.name = name;
- }
-
- public String getName() {
- return name;
- }
-
- @Override
- public String toString() {
- return name;
- }
-
-}
diff --git a/de.prob.core/src/de/prob/model/eventb/Variant.java b/de.prob.core/src/de/prob/model/eventb/Variant.java
deleted file mode 100644
index 7fcbc5363ba9be0cacaa7c1065dfd04834d8bb08..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/model/eventb/Variant.java
+++ /dev/null
@@ -1,23 +0,0 @@
-package de.prob.model.eventb;
-
-import de.prob.animator.domainobjects.EventB;
-import de.prob.animator.domainobjects.IEvalElement;
-import de.prob.model.representation.AbstractElement;
-import de.prob.model.representation.IEval;
-
-public class Variant extends AbstractElement implements IEval {
- private final IEvalElement expression;
-
- public Variant(final String code) {
- expression = new EventB(code);
- }
-
- public IEvalElement getExpression() {
- return expression;
- }
-
- @Override
- public IEvalElement getEvaluate() {
- return expression;
- }
-}
diff --git a/de.prob.core/src/de/prob/model/eventb/Witness.java b/de.prob.core/src/de/prob/model/eventb/Witness.java
deleted file mode 100644
index d476e0cae01a2704b2fb1f56dddfcd7e2c2b77bc..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/model/eventb/Witness.java
+++ /dev/null
@@ -1,31 +0,0 @@
-package de.prob.model.eventb;
-
-import de.prob.animator.domainobjects.EventB;
-import de.prob.animator.domainobjects.IEvalElement;
-import de.prob.model.representation.AbstractElement;
-import de.prob.model.representation.IEval;
-
-public class Witness extends AbstractElement implements IEval {
-
- private final String name;
- private final EventB predicate;
-
- public Witness(final String name, final String code) {
- this.name = name;
- predicate = new EventB(code);
- }
-
- public String getName() {
- return name;
- }
-
- public EventB getPredicate() {
- return predicate;
- }
-
- @Override
- public IEvalElement getEvaluate() {
- return predicate;
- }
-
-}
diff --git a/de.prob.core/src/de/prob/model/representation/AbstractElement.java b/de.prob.core/src/de/prob/model/representation/AbstractElement.java
deleted file mode 100644
index 53c0c5aca6cd86c5ef43bf01020f0514afe9dd51..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/model/representation/AbstractElement.java
+++ /dev/null
@@ -1,58 +0,0 @@
-package de.prob.model.representation;
-
-import java.util.Collection;
-import java.util.Collections;
-import java.util.HashMap;
-import java.util.LinkedHashSet;
-import java.util.Map;
-import java.util.Set;
-
-/**
- * This class is the subclass of all model elements (Models, Machines, Contexts,
- * Variables, etc.)
- *
- * @author joy
- *
- */
-public abstract class AbstractElement {
- protected Map<Class<? extends AbstractElement>, java.util.Set<? extends AbstractElement>> children = new HashMap<Class<? extends AbstractElement>, Set<? extends AbstractElement>>();
-
- /**
- * Each {@link AbstractElement} can have children of a subclass that extends
- * {@link AbstractElement}. These are specified by the class of the child.
- * To get a Set of all of the children of a particular class, use this
- * method.
- *
- * @param c
- * {@link Class} T of the desired type of children
- * @return {@link Set} containing all the children of type T
- */
- @SuppressWarnings("unchecked")
- public <T extends AbstractElement> Set<T> getChildrenOfType(final Class<T> c) {
- Set<? extends AbstractElement> set = children.get(c);
- if (set == null) {
- return Collections.emptySet();
- }
- return (Set<T>) set;
- }
-
- /**
- * Maps a {@link Collection} of elements to the specified {@link Class}
- *
- * @param c
- * {@link Class} to specify children elements
- * @param elements
- * {@link Collection} of elements with which c will be mapped
- */
- public <T extends AbstractElement> void put(final Class<T> c,
- final Collection<? extends T> elements) {
- children.put(c, new LinkedHashSet<T>(elements));
- }
-
- /**
- * @return the {@link Map} of {@link Class} to {@link Set} of children
- */
- public Map<Class<? extends AbstractElement>, java.util.Set<? extends AbstractElement>> getChildren() {
- return children;
- }
-}
diff --git a/de.prob.core/src/de/prob/model/representation/Action.java b/de.prob.core/src/de/prob/model/representation/Action.java
deleted file mode 100644
index 5950f5e4431da0186991409d0e8c2d44bde5f179..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/model/representation/Action.java
+++ /dev/null
@@ -1,19 +0,0 @@
-package de.prob.model.representation;
-
-public abstract class Action extends AbstractElement {
-
- private final String code;
-
- public Action(final String code) {
- this.code = code;
- }
-
- public String getCode() {
- return code;
- }
-
- @Override
- public String toString() {
- return code;
- }
-}
diff --git a/de.prob.core/src/de/prob/model/representation/Axiom.java b/de.prob.core/src/de/prob/model/representation/Axiom.java
deleted file mode 100644
index d76f5fa2b3fe1dad5fe86cfdb244a1f11cebdec1..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/model/representation/Axiom.java
+++ /dev/null
@@ -1,27 +0,0 @@
-package de.prob.model.representation;
-
-import de.prob.animator.domainobjects.IEvalElement;
-import de.prob.unicode.UnicodeTranslator;
-
-public abstract class Axiom extends AbstractElement implements IEval {
-
- private final IEvalElement predicate;
-
- public Axiom(final IEvalElement predicate) {
- this.predicate = predicate;
- }
-
- public IEvalElement getPredicate() {
- return predicate;
- }
-
- @Override
- public IEvalElement getEvaluate() {
- return predicate;
- }
-
- @Override
- public String toString() {
- return UnicodeTranslator.toUnicode(predicate.getCode());
- }
-}
diff --git a/de.prob.core/src/de/prob/model/representation/BEvent.java b/de.prob.core/src/de/prob/model/representation/BEvent.java
deleted file mode 100644
index ccea9c12a7972c11f2dd100d634946d9fd0be888..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/model/representation/BEvent.java
+++ /dev/null
@@ -1,20 +0,0 @@
-package de.prob.model.representation;
-
-
-public abstract class BEvent extends AbstractElement {
-
- private final String name;
-
- public BEvent(final String name) {
- this.name = name;
- }
-
- public String getName() {
- return name;
- }
-
- @Override
- public String toString() {
- return name;
- }
-}
diff --git a/de.prob.core/src/de/prob/model/representation/BSet.java b/de.prob.core/src/de/prob/model/representation/BSet.java
deleted file mode 100644
index 44040c771baff1d07714d72d6d5b5459f797dfde..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/model/representation/BSet.java
+++ /dev/null
@@ -1,19 +0,0 @@
-package de.prob.model.representation;
-
-public class BSet extends AbstractElement {
-
- private final String name;
-
- public BSet(final String name) {
- this.name = name;
- }
-
- public String getName() {
- return name;
- }
-
- @Override
- public String toString() {
- return name;
- }
-}
diff --git a/de.prob.core/src/de/prob/model/representation/Constant.java b/de.prob.core/src/de/prob/model/representation/Constant.java
deleted file mode 100644
index ad9742da06bd61932c201557f401c000a88720fc..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/model/representation/Constant.java
+++ /dev/null
@@ -1,39 +0,0 @@
-package de.prob.model.representation;
-
-import de.prob.animator.domainobjects.EvaluationResult;
-import de.prob.animator.domainobjects.IEvalElement;
-import de.prob.unicode.UnicodeTranslator;
-
-public abstract class Constant extends AbstractElement implements IEval {
-
- protected final IEvalElement expression;
- protected EvaluationResult result;
-
- public Constant(final IEvalElement expression) {
- this.expression = expression;
- }
-
- public IEvalElement getExpression() {
- return expression;
- }
-
- @Override
- public IEvalElement getEvaluate() {
- return expression;
- }
-
- @Override
- public String toString() {
- return UnicodeTranslator.toUnicode(expression.getCode());
- }
-
-// // Experimental. Would allow the user to calculate the value once and cache
-// // it.
-// public EvaluationResult getValue(final History h) {
-// if (result == null) {
-// result = h.evalCurrent(getEvaluate());
-// }
-// return result;
-// }
-
-}
diff --git a/de.prob.core/src/de/prob/model/representation/FormulaUUID.java b/de.prob.core/src/de/prob/model/representation/FormulaUUID.java
deleted file mode 100644
index d84d6c7f28c2e427f674ea6a367dda9f9beb7056..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/model/representation/FormulaUUID.java
+++ /dev/null
@@ -1,6 +0,0 @@
-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/Guard.java b/de.prob.core/src/de/prob/model/representation/Guard.java
deleted file mode 100644
index b6574defafa1be14be6a40e3634d6eaadbc6fc5b..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/model/representation/Guard.java
+++ /dev/null
@@ -1,26 +0,0 @@
-package de.prob.model.representation;
-
-import de.prob.animator.domainobjects.IEvalElement;
-
-public abstract class Guard extends AbstractElement implements IEval {
-
- private final IEvalElement predicate;
-
- public Guard(final IEvalElement predicate) {
- this.predicate = predicate;
- }
-
- public IEvalElement getPredicate() {
- return predicate;
- }
-
- @Override
- public IEvalElement getEvaluate() {
- return predicate;
- }
-
- @Override
- public String toString() {
- return predicate.toString();
- }
-}
diff --git a/de.prob.core/src/de/prob/model/representation/IEval.java b/de.prob.core/src/de/prob/model/representation/IEval.java
deleted file mode 100644
index 5dddd32727290ff31ce1f30600881d51017f217c..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/model/representation/IEval.java
+++ /dev/null
@@ -1,7 +0,0 @@
-package de.prob.model.representation;
-
-import de.prob.animator.domainobjects.IEvalElement;
-
-public interface IEval {
- public IEvalElement getEvaluate();
-}
diff --git a/de.prob.core/src/de/prob/model/representation/Invariant.java b/de.prob.core/src/de/prob/model/representation/Invariant.java
deleted file mode 100644
index 18de7013a3dbd0ea2dca52b793260c0ae4bc41fa..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/model/representation/Invariant.java
+++ /dev/null
@@ -1,28 +0,0 @@
-package de.prob.model.representation;
-
-import de.prob.animator.domainobjects.IEvalElement;
-import de.prob.unicode.UnicodeTranslator;
-
-public abstract class Invariant extends AbstractElement implements IEval {
-
- private final IEvalElement predicate;
-
- public Invariant(final IEvalElement predicate) {
- this.predicate = predicate;
- }
-
- public IEvalElement getPredicate() {
- return predicate;
- }
-
- @Override
- public IEvalElement getEvaluate() {
- return predicate;
- }
-
- @Override
- public String toString() {
- return UnicodeTranslator.toUnicode(predicate.getCode());
- }
-
-}
diff --git a/de.prob.core/src/de/prob/model/representation/Machine.java b/de.prob.core/src/de/prob/model/representation/Machine.java
deleted file mode 100644
index c5cad197b3fad9fc15cee1f4c9ab76f8da70029e..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/model/representation/Machine.java
+++ /dev/null
@@ -1,19 +0,0 @@
-package de.prob.model.representation;
-
-public abstract class Machine extends AbstractElement {
-
- private final String name;
-
- public Machine(final String name) {
- this.name = name;
- }
-
- public String getName() {
- return name;
- }
-
- @Override
- public String toString() {
- return name;
- }
-}
diff --git a/de.prob.core/src/de/prob/model/representation/RefType.java b/de.prob.core/src/de/prob/model/representation/RefType.java
deleted file mode 100644
index 192a8a4aafe21eb232ada4f0045f5b0c4e6e2b1d..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/model/representation/RefType.java
+++ /dev/null
@@ -1,28 +0,0 @@
-package de.prob.model.representation;
-
-public class RefType {
- private final ERefType relationship;
-
- /*
- * RefType is used for both ClassicalBModels and EventBModels
- *
- * ClassicalB: SEES, USES, REFINES, INCLUDES, IMPORTS EventB: SEES, REFINES,
- * EXTENDS
- */
- public enum ERefType {
- SEES, USES, REFINES, INCLUDES, IMPORTS, EXTENDS
- }
-
- public RefType(final ERefType relationship) {
- this.relationship = relationship;
- }
-
- @Override
- public String toString() {
- return relationship.toString();
- }
-
- public ERefType getRelationship() {
- return relationship;
- }
-}
diff --git a/de.prob.core/src/de/prob/model/representation/StateSchema.java b/de.prob.core/src/de/prob/model/representation/StateSchema.java
deleted file mode 100644
index 52f97690b9232ee8263766af00cb05ed825d63bc..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/model/representation/StateSchema.java
+++ /dev/null
@@ -1,6 +0,0 @@
-package de.prob.model.representation;
-
-public interface StateSchema {
- public Object[] getElements(Object o);
- public boolean hasChildren(Object o);
-}
diff --git a/de.prob.core/src/de/prob/model/representation/Variable.java b/de.prob.core/src/de/prob/model/representation/Variable.java
deleted file mode 100644
index 098bb5e99ca13b0c0a03145680191ea1aeaace6c..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/model/representation/Variable.java
+++ /dev/null
@@ -1,31 +0,0 @@
-package de.prob.model.representation;
-
-import de.prob.animator.domainobjects.IEvalElement;
-import de.prob.unicode.UnicodeTranslator;
-
-public abstract class Variable extends AbstractElement implements IEval {
-
- protected final IEvalElement expression;
-
- public Variable(final IEvalElement expression) {
- this.expression = expression;
- }
-
- public IEvalElement getExpression() {
- return expression;
- }
-
- @Override
- public IEvalElement getEvaluate() {
- return expression;
- }
-
- public String getName() {
- return expression.getCode();
- }
-
- @Override
- public String toString() {
- return UnicodeTranslator.toUnicode(expression.getCode());
- }
-}
diff --git a/de.prob.core/src/de/prob/model/serialize/EventBModelTranslator.java b/de.prob.core/src/de/prob/model/serialize/EventBModelTranslator.java
deleted file mode 100644
index 354414a4617e438b0866697f3f6632081561bf50..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/model/serialize/EventBModelTranslator.java
+++ /dev/null
@@ -1,295 +0,0 @@
-package de.prob.model.serialize;
-
-import java.io.ByteArrayOutputStream;
-import java.io.File;
-import java.io.IOException;
-import java.util.ArrayList;
-import java.util.Base64;
-import java.util.Collection;
-import java.util.HashMap;
-import java.util.List;
-import java.util.Map;
-import java.util.zip.GZIPOutputStream;
-
-import org.eclipse.core.runtime.CoreException;
-import org.eventb.core.IConvergenceElement.Convergence;
-import org.eventb.core.IEventBProject;
-import org.eventb.core.IEventBRoot;
-import org.eventb.core.ISCAction;
-import org.eventb.core.ISCAxiom;
-import org.eventb.core.ISCCarrierSet;
-import org.eventb.core.ISCConstant;
-import org.eventb.core.ISCContextRoot;
-import org.eventb.core.ISCEvent;
-import org.eventb.core.ISCExtendsContext;
-import org.eventb.core.ISCGuard;
-import org.eventb.core.ISCInternalContext;
-import org.eventb.core.ISCInvariant;
-import org.eventb.core.ISCMachineRoot;
-import org.eventb.core.ISCParameter;
-import org.eventb.core.ISCRefinesEvent;
-import org.eventb.core.ISCRefinesMachine;
-import org.eventb.core.ISCVariable;
-import org.eventb.core.ISCVariant;
-import org.eventb.core.ISCWitness;
-import org.rodinp.core.IInternalElement;
-import org.rodinp.core.IInternalElementType;
-import org.rodinp.core.IRodinFile;
-
-import com.thoughtworks.xstream.XStream;
-
-import de.prob.model.eventb.Context;
-import de.prob.model.eventb.Event;
-import de.prob.model.eventb.Event.EventType;
-import de.prob.model.eventb.EventBAction;
-import de.prob.model.eventb.EventBAxiom;
-import de.prob.model.eventb.EventBConstant;
-import de.prob.model.eventb.EventBGuard;
-import de.prob.model.eventb.EventBInvariant;
-import de.prob.model.eventb.EventBMachine;
-import de.prob.model.eventb.EventBVariable;
-import de.prob.model.eventb.EventParameter;
-import de.prob.model.eventb.Variant;
-import de.prob.model.eventb.Witness;
-import de.prob.model.representation.AbstractElement;
-import de.prob.model.representation.BSet;
-
-public class EventBModelTranslator {
- //
- // Map<String, ISCMachineRoot> machines = new HashMap<String,
- // ISCMachineRoot>();
- // Map<String, ISCContextRoot> contexts = new HashMap<String,
- // ISCContextRoot>();
-
- Map<String, EventBMachine> machines = new HashMap<String, EventBMachine>();
- Map<String, Context> contexts = new HashMap<String, Context>();
- File modelFile;
-
- AbstractElement mainComponent;
- private final IEventBProject eventBProject;
-
- public EventBModelTranslator(final IEventBRoot root) {
- modelFile = root.getUnderlyingResource().getRawLocation().toFile();
- eventBProject = root.getEventBProject();
- IInternalElementType<? extends IInternalElement> elementType = root
- .getElementType();
- String id = elementType.getId();
- if (id.equals("org.eventb.core.machineFile")) {
- ISCMachineRoot scMachineRoot = eventBProject.getSCMachineRoot(root
- .getElementName());
- mainComponent = translateMachine(scMachineRoot);
- }
- if (id.equals("org.eventb.core.contextFile")) {
- ISCContextRoot scContextRoot = eventBProject.getSCContextRoot(root
- .getElementName());
- mainComponent = translateContext(scContextRoot);
- }
- }
-
- private Context translateContext(final ISCContextRoot root) {
- String name = root.getComponentName();
- if (contexts.containsKey(name)) {
- return contexts.get(name);
- }
-
- Context c = new Context(name);
- try {
- List<Context> exts = new ArrayList<Context>();
- for (ISCExtendsContext iscExtendsContext : root
- .getSCExtendsClauses()) {
- String componentName = iscExtendsContext.getAbstractSCContext()
- .getRodinFile().getBareName();
- exts.add(translateContext(eventBProject
- .getSCContextRoot(componentName)));
- }
- c.addExtends(exts);
-
- List<BSet> sets = new ArrayList<BSet>();
- for (ISCCarrierSet iscCarrierSet : root.getSCCarrierSets()) {
- sets.add(new BSet(iscCarrierSet.getIdentifierString()));
- }
- c.addSets(sets);
-
- List<EventBAxiom> axioms = new ArrayList<EventBAxiom>();
- for (ISCAxiom iscAxiom : root.getSCAxioms()) {
- String elementName = iscAxiom.getRodinFile().getBareName();
- String predicateString = iscAxiom.getPredicateString();
- boolean theorem = iscAxiom.isTheorem();
- axioms.add(new EventBAxiom(elementName, predicateString,
- theorem));
- }
- c.addAxioms(axioms);
-
- List<EventBConstant> constants = new ArrayList<EventBConstant>();
- for (ISCConstant iscConstant : root.getSCConstants()) {
- constants.add(new EventBConstant(iscConstant.getElementName()));
- }
- c.addConstants(constants);
- } catch (CoreException e) {
- e.printStackTrace();
- }
- contexts.put(c.getName(), c);
- return c;
- }
-
- private EventBMachine translateMachine(final ISCMachineRoot root) {
- String name = root.getComponentName();
- if (machines.containsKey(name)) {
- return machines.get(name);
- }
-
- EventBMachine machine = new EventBMachine(name);
-
- try {
- List<EventBMachine> refines = new ArrayList<EventBMachine>();
- ISCRefinesMachine[] scRefinesClauses = root.getSCRefinesClauses();
- for (ISCRefinesMachine iscRefinesMachine : scRefinesClauses) {
- IRodinFile abstractSCMachine = iscRefinesMachine
- .getAbstractSCMachine();
- String bareName = abstractSCMachine.getBareName();
- refines.add(translateMachine(eventBProject
- .getSCMachineRoot(bareName)));
- }
- machine.addRefines(refines);
-
- List<Context> sees = new ArrayList<Context>();
- for (ISCInternalContext iscInternalContext : root
- .getSCSeenContexts()) {
- String componentName = iscInternalContext.getComponentName();
- sees.add(translateContext(eventBProject
- .getSCContextRoot(componentName)));
- }
- machine.addSees(sees);
-
- List<EventBVariable> variables = new ArrayList<EventBVariable>();
- for (ISCVariable iscVariable : root.getSCVariables()) {
- variables.add(new EventBVariable(iscVariable.getElementName()));
- }
- machine.addVariables(variables);
-
- List<EventBInvariant> invariants = new ArrayList<EventBInvariant>();
- for (ISCInvariant iscInvariant : root.getSCInvariants()) {
- String elementName = iscInvariant.getElementName();
- String predicateString = iscInvariant.getPredicateString();
- boolean theorem = iscInvariant.isTheorem();
- invariants.add(new EventBInvariant(elementName,
- predicateString, theorem));
- }
- machine.addInvariants(invariants);
-
- List<Variant> variant = new ArrayList<Variant>();
- for (ISCVariant iscVariant : root.getSCVariants()) {
- variant.add(new Variant(iscVariant.getExpressionString()));
- }
- machine.addVariant(variant);
-
- List<Event> events = new ArrayList<Event>();
- ISCEvent[] scEvents = root.getSCEvents();
- for (ISCEvent iscEvent : scEvents) {
- events.add(extractEvent(iscEvent));
- }
- machine.addEvents(events);
- } catch (CoreException e) {
- e.printStackTrace();
- }
- machines.put(machine.getName(), machine);
- return machine;
- }
-
- private Event extractEvent(final ISCEvent iscEvent) throws CoreException {
- String name = iscEvent.getLabel();
-
- int typeId = iscEvent.getConvergence().getCode();
-
- Event e = new Event(name, calculateEventType(typeId));
-
- List<Event> refines = new ArrayList<Event>();
- for (ISCRefinesEvent iscRefinesEvent : iscEvent.getSCRefinesClauses()) {
- refines.add(extractEvent(iscRefinesEvent.getAbstractSCEvent()));
- }
- e.addRefines(refines);
-
- List<EventBGuard> guards = new ArrayList<EventBGuard>();
- for (ISCGuard iscGuard : iscEvent.getSCGuards()) {
- String elementName = iscGuard.getElementName();
- String predicateString = iscGuard.getPredicateString();
- boolean theorem = iscGuard.isTheorem();
- guards.add(new EventBGuard(elementName, predicateString, theorem));
- }
- e.addGuards(guards);
-
- List<EventBAction> actions = new ArrayList<EventBAction>();
- for (ISCAction iscAction : iscEvent.getSCActions()) {
- String elementName = iscAction.getElementName();
- String assignmentString = iscAction.getAssignmentString();
- actions.add(new EventBAction(elementName, assignmentString));
- }
- e.addActions(actions);
-
- List<Witness> witnesses = new ArrayList<Witness>();
- for (ISCWitness iscWitness : iscEvent.getSCWitnesses()) {
- String elementName = iscWitness.getElementName();
- String predicateString = iscWitness.getPredicateString();
- witnesses.add(new Witness(elementName, predicateString));
- }
- e.addWitness(witnesses);
-
- List<EventParameter> parameters = new ArrayList<EventParameter>();
- for (ISCParameter iscParameter : iscEvent.getSCParameters()) {
- parameters.add(new EventParameter(iscParameter
- .getIdentifierString()));
- }
- e.addParameters(parameters);
-
- return e;
- }
-
- private EventType calculateEventType(final int typeId) {
- Convergence valueOf = Convergence.valueOf(typeId);
- if (valueOf.equals(Convergence.ORDINARY)) {
- return EventType.ORDINARY;
- }
- if (valueOf.equals(Convergence.CONVERGENT)) {
- return EventType.CONVERGENT;
- }
- if (valueOf.equals(Convergence.ANTICIPATED)) {
- return EventType.ANTICIPATED;
- }
- return null;
- }
-
- public AbstractElement getMainComponent() {
- return mainComponent;
- }
-
- public Collection<EventBMachine> getMachines() {
- return machines.values();
- }
-
- public Collection<Context> getContexts() {
- return contexts.values();
- }
-
- public File getModelFile() {
- return modelFile;
- }
-
- public String serialized() {
- XStream xstream = new XStream();
- String xml = xstream.toXML(new ModelObject(getMachines(),
- getContexts(), modelFile, mainComponent));
- ByteArrayOutputStream out = new ByteArrayOutputStream();
- GZIPOutputStream gzip;
- byte[] bytes;
- try {
- gzip = new GZIPOutputStream(out);
- gzip.write(xml.getBytes());
- gzip.close();
- bytes = out.toByteArray();
- } catch (IOException e) {
- bytes = xml.getBytes();
- }
- return Base64.getMimeEncoder().encodeToString(bytes);
- }
-
-}
diff --git a/de.prob.core/src/de/prob/model/serialize/ModelObject.java b/de.prob.core/src/de/prob/model/serialize/ModelObject.java
deleted file mode 100644
index 16deeb951e9fc51894ea69b2ab0866e0dfb25444..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/model/serialize/ModelObject.java
+++ /dev/null
@@ -1,38 +0,0 @@
-package de.prob.model.serialize;
-
-import java.io.File;
-import java.util.Collection;
-
-import de.prob.model.eventb.Context;
-import de.prob.model.eventb.EventBMachine;
-import de.prob.model.representation.AbstractElement;
-
-public class ModelObject {
- final Collection<EventBMachine> machines;
- final Collection<Context> contexts;
- final File modelFile;
- final AbstractElement mainComponent;
-
- public ModelObject(Collection<EventBMachine> machines, Collection<Context> contexts, File modelFile, AbstractElement mainComponent) {
- this.machines = machines;
- this.contexts = contexts;
- this.modelFile = modelFile;
- this.mainComponent = mainComponent;
- }
-
- public Collection<EventBMachine> getMachines() {
- return machines;
- }
-
- public Collection<Context> getContexts() {
- return contexts;
- }
-
- public File getModelFile() {
- return modelFile;
- }
-
- public AbstractElement getMainComponent() {
- return mainComponent;
- }
-}