Merge branch 'develop' of github.com:bendisposto/prob into develop

de.prob.core/src/de/prob/animator/domainobjects/EBEvent.java

+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));
+	}
+}

de.prob.core/src/de/prob/animator/domainobjects/EvalElementType.java

+package de.prob.animator.domainobjects;
+
+public enum EvalElementType {
+	PREDICATE, EXPRESSION;
+
+	@Override
+	public String toString() {
+		return "#" + super.toString();
+	}
+
+}

de.prob.core/src/de/prob/animator/domainobjects/IEvalElement.java

+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();
+}

de.prob.core/src/de/prob/model/eventb/EBContext.java

+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));
+	}
+
+}

de.prob.core/src/de/prob/model/eventb/EBMachine.java

+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));
+	}
+}

de.prob.core/src/de/prob/model/eventb/EventB.java

+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;
+	}
+
+}

de.prob.core/src/de/prob/model/eventb/Model.java

+package de.prob.model.eventb;
+
+import java.util.ArrayList;
+import java.util.List;
+
+public class Model {
+
+	public List<Relationship> relationships = new ArrayList<Relationship>();
+}

de.prob.core/src/de/prob/model/eventb/Relationship.java

+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;
+	}
+}

de.prob.core/src/de/prob/model/representation/FormulaUUID.java

+package de.prob.model.representation;
+
+public class FormulaUUID {
+	static int count = 0;
+	public final String uuid = "Formula_" + (++count);
+}

de.prob.core/src/de/prob/model/representation/IEntity.java

+package de.prob.model.representation;
+
+import java.util.List;
+
+public interface IEntity {
+	public List<IEntity> getChildren();
+
+	public boolean hasChildren();
+}

de.prob.core/src/de/prob/model/representation/Label.java

+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();
+	}
+}