Commit 050dee14 authored by Sarah Grebing's avatar Sarah Grebing

interim

parent 7e5e33d0
Pipeline #12924 failed with stage
in 1 minute and 36 seconds
......@@ -26,7 +26,7 @@ termPattern :
f(x), f(x,y,g(y)), X, ?Y, _, ..., f(... ?X ...), f(..., ?X), f(..., ...?X...), f(..., ... g(x) ...), f(_, x, _, y, ... y ...)
*/
semiSeqPattern : termPattern (',' termPattern)*;
sequentPattern : semiSeqPattern? ARROW semiSeqPattern?;
sequentPattern : antec=semiSeqPattern? ARROW succ=semiSeqPattern?;
ARROW : '⇒' | '==>';
DONTCARE: '?' | '_' | '█';
......
......@@ -93,11 +93,22 @@ public class ProofTree extends BorderPane {
init();
}
private void init() {
if (root.get() != null)
treeProof.setRoot(new TreeItemNode(root.get()));
treeProof.refresh();
}
private TreeCell<Node> cellFactory(TreeView<Node> nodeTreeView) {
TextFieldTreeCell<Node> tftc = new TextFieldTreeCell<>();
tftc.setConverter(new StringConverter<Node>() {
@Override
public String toString(Node object) {
/* if (object.getAppliedRuleApp() != null) {
return object.getAppliedRuleApp().rule().displayName();
} else {
return object.name();
}*/
return object.sequent().toString();
}
......@@ -124,12 +135,6 @@ public class ProofTree extends BorderPane {
}
}
private void init() {
if (root.get() != null)
treeProof.setRoot(new TreeItemNode(root.get()));
treeProof.refresh();
}
public Object getColorOfNodes() {
return colorOfNodes.get();
}
......@@ -172,6 +177,11 @@ class TreeItemNode extends TreeItem<Node> {
super(value);
}
@Override
public boolean isLeaf() {
return getValue().leaf();
}
@Override
public ObservableList<TreeItem<Node>> getChildren() {
if (super.getChildren().size() != getValue().children().size())
......@@ -179,9 +189,4 @@ class TreeItemNode extends TreeItem<Node> {
getValue().children().stream().map(TreeItemNode::new).collect(Collectors.toList()));
return super.getChildren();
}
@Override
public boolean isLeaf() {
return getValue().leaf();
}
}
\ No newline at end of file
......@@ -7,6 +7,7 @@ import javafx.scene.layout.AnchorPane;
import java.io.File;
/**
* Welcome pane that allows for a more usable entry point
* Created by weigl on 7/7/17.
*/
public class WelcomePane extends AnchorPane {
......@@ -21,11 +22,11 @@ public class WelcomePane extends AnchorPane {
proofScriptDebugger.getWelcomePaneDock().close();
proofScriptDebugger.showActiveInspector(null);
proofScriptDebugger.openScript(
new File("src/test/resources/edu/kit/formal/interpreter/contraposition/w_branching.kps")
new File("src/test/resources/edu/kit/formal/psdb/interpreter/contraposition/w_branching.kps")
);
proofScriptDebugger.openKeyFile(
new File("src/test/resources/edu/kit/formal/interpreter/contraposition/contraposition.key"));
new File("src/test/resources/edu/kit/formal/psdb/interpreter/contraposition/contraposition.key"));
}
......@@ -33,10 +34,10 @@ public class WelcomePane extends AnchorPane {
proofScriptDebugger.getWelcomePaneDock().close();
proofScriptDebugger.showActiveInspector(null);
proofScriptDebugger.openScript(
new File("src/test/resources/edu/kit/formal/interpreter/javaExample/test.kps")
new File("src/test/resources/edu/kit/formal/psdb/interpreter/javaExample/test.kps")
);
proofScriptDebugger.openJavaFile(
new File("src/test/resources/edu/kit/formal/interpreter/javaExample/Test.java"));
new File("src/test/resources/edu/kit/formal/psdb/interpreter/javaExample/Test.java"));
}
public void loadHelpPage(ActionEvent event) {
......@@ -54,5 +55,20 @@ public class WelcomePane extends AnchorPane {
proofScriptDebugger.openScript();
}
public void loadNewScript(ActionEvent event) {
proofScriptDebugger.getWelcomePaneDock().close();
proofScriptDebugger.showActiveInspector(null);
proofScriptDebugger.getScriptController().newScript();
}
public void openScript(ActionEvent event) {
proofScriptDebugger.getWelcomePaneDock().close();
proofScriptDebugger.showActiveInspector(null);
proofScriptDebugger.openScript();
}
}
......@@ -51,10 +51,6 @@ public class PTreeNode {
this.scriptstmt = scriptstmt;
}
public boolean hasState() {
return state != null;
}
public LinkedList<ASTNode> getContext() {
return context;
}
......@@ -80,5 +76,11 @@ public class PTreeNode {
return sb.toString();
}
public boolean hasState() {
return state != null;
}
}
package edu.kit.formal.psdb.interpreter.graphs;
import com.google.common.eventbus.Subscribe;
import com.google.common.graph.MutableValueGraph;
import edu.kit.formal.psdb.gui.controller.Events;
import edu.kit.formal.psdb.gui.controller.PuppetMaster;
import edu.kit.formal.psdb.gui.controls.DebuggerStatusBar;
import edu.kit.formal.psdb.gui.model.Breakpoint;
import edu.kit.formal.psdb.interpreter.Interpreter;
import edu.kit.formal.psdb.interpreter.InterpretingService;
import edu.kit.formal.psdb.interpreter.data.GoalNode;
......@@ -155,6 +157,18 @@ public class ProofTreeController {
//TODO handle endpoint
private static boolean compareCtrlFlowNodes(ControlFlowNode newNode, ControlFlowNode oldNode) {
return newNode.getScriptstmt().getNodeName().equals(oldNode.getScriptstmt().getNodeName());
}
//TODO handle endpoint of graph
private static boolean comparePTreeNodes(PTreeNode newTreeNode, PTreeNode oldTreeNode) {
return false;
}
/**
* StepOver and return the node to which the state pointer is pointing to
*
......@@ -186,8 +200,6 @@ public class ProofTreeController {
return statePointer;
}
//TODO handle endpoint of graph
/**
* Step Back one Node in the stategraph
*
......@@ -312,17 +324,6 @@ public class ProofTreeController {
MutableValueGraph ctrlFlow = controlFlowGraphVisitor.getGraph();
}
private boolean compareCtrlFlowNodes(ControlFlowNode newNode, ControlFlowNode oldNode) {
return newNode.getScriptstmt().getNodeName().equals(oldNode.getScriptstmt().getNodeName());
}
private boolean comparePTreeNodes(PTreeNode newTreeNode, PTreeNode oldTreeNode) {
return false;
}
/**************************************************************************************************************
*
* Getter and Setter
......
package edu.kit.formal.psdb.termmatcher;
import de.uka.ilkd.key.logic.Semisequent;
import de.uka.ilkd.key.logic.Sequent;
import de.uka.ilkd.key.logic.Term;
import org.antlr.v4.runtime.CharStream;
import org.antlr.v4.runtime.CharStreams;
......@@ -25,4 +27,45 @@ public class MatcherFacade {
public static MatchPatternParser getParser(CharStream stream) {
return new MatchPatternParser(new CommonTokenStream(new MatchPatternLexer(stream)));
}
/**
* Match a semisequent against a sequent
*
* @param pattern Semiseqeuent pattern e.g. f(x), f(x)
* @param semiSeq Concrete KeY Semisequent
* @return Matchings
*/
public static Matchings matches(String pattern, Semisequent semiSeq) {
MatcherImpl matcher = new MatcherImpl();
MatchPatternParser mpp = getParser(pattern);
MatchPatternParser.SemiSeqPatternContext ctx = mpp.semiSeqPattern();
return matches(ctx, semiSeq);
}
public static Matchings matches(MatchPatternParser.SemiSeqPatternContext pattern, Semisequent semiSeq) {
//semiSeq.iterator()
// List<MatchPatternParser.TermPatternContext> termPatternContexts = ctx.termPattern();
// for (MatchPatternParser.TermPatternContext termpattern: termPatternContexts) {
//for all terms in seq
// Matchings s = accept(termpattern, peek);
// }
return null;
}
/**
* Match a sequent pattern against a concrete sequent
*
* @param pattern e.g., f(x) ==> f(y)
* @param sequent
* @return
*/
public static Matchings matches(String pattern, Sequent sequent) {
MatcherImpl matcher = new MatcherImpl();
MatchPatternParser mpp = getParser(pattern);
MatchPatternParser.SequentPatternContext ctx = mpp.sequentPattern();
return null;
}
}
......@@ -2,19 +2,16 @@ package edu.kit.formal.psdb.termmatcher;
import de.uka.ilkd.key.logic.Term;
import java.lang.reflect.Array;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.Spliterator;
import java.util.Stack;
import java.util.function.Consumer;
import java.util.function.Supplier;
import java.util.stream.IntStream;
import java.util.stream.Stream;
import java.util.stream.StreamSupport;
/**
* Matchpattern visitor visits the matchpatterns of case-statements
* @author Alexander Weigl
* @author S. Grebing
*/
class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
static final Matchings NO_MATCH = new Matchings();
......@@ -22,6 +19,13 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
private Stack<Term> termStack = new Stack<>();
/**
* Visit '_'
*
* @param ctx
* @param peek
* @return
*/
@Override
public Matchings visitDontCare(MatchPatternParser.DontCareContext ctx, Term peek) {
if (peek != null) {
......@@ -40,6 +44,13 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
}
}*/
/**
* Visit a Schema Variable
*
* @param ctx
* @param peek
* @return
*/
@Override
protected Matchings visitSchemaVar(MatchPatternParser.SchemaVarContext ctx, Term peek) {
if (peek != null) {
......@@ -49,6 +60,12 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
}
}
/**
* Visit a '...'Term'...' structure
* @param ctx
* @param peek
* @return
*/
@Override
protected Matchings visitAnywhere(MatchPatternParser.AnywhereContext ctx, Term peek) {
Matchings m = new Matchings();
......@@ -60,10 +77,15 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
}
/**
* Visit a function and predicate symbol without a sequent arrow
* @param ctx
* @param peek
* @return
*/
@Override
protected Matchings visitFunction(MatchPatternParser.FunctionContext ctx, Term peek) {
String expectedFunction = ctx.func.getText();
if (peek.op().name().toString().equals(expectedFunction) // same name
&& ctx.termPattern().size() == peek.arity() // same arity
) {
......@@ -75,12 +97,23 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
return NO_MATCH;
}
/**
* Visit a semisequent pattern f(x), f(y)
* @param ctx
* @param peek
* @return
*/
@Override
protected Matchings visitSemiSeqPattern(MatchPatternParser.SemiSeqPatternContext ctx, Term peek) {
return null;
}
/**
* Visit a sequent pattern 'f(x) ==> f(x)', 'f(x) ==>' or '==> f(x)'
* @param ctx
* @param peek
* @return
*/
@Override
protected Matchings visitSequentPattern(MatchPatternParser.SequentPatternContext ctx, Term peek) {
return null;
......@@ -101,6 +134,9 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
}
/**
* Reduce the matchings by eliminating non-compatible matchings.
* For example:
* m1: <X, f(y)>, <Y,g> and m2: <X, g> <Y, f(x)>
* @param m1
* @param m2
* @return
......@@ -134,7 +170,9 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
}
}
/**
* Class Matching contains a hashmap of string to term
*/
class Matchings extends ArrayList<HashMap<String, Term>> {
public static Matchings singleton(String name, Term peek) {
Matchings matchings = new Matchings();
......
......@@ -36,12 +36,14 @@
<RowConstraints maxHeight="1.7976931348623157E308" minHeight="50.0" prefHeight="30.0" valignment="CENTER" vgrow="ALWAYS" />
</rowConstraints>
<children>
<Button contentDisplay="TOP" maxWidth="1.7976931348623157E308" text="Open Script..." GridPane.columnIndex="0" GridPane.rowIndex="0">
<Button contentDisplay="TOP" maxWidth="1.7976931348623157E308" text="Open Script..."
onAction="#openScript" GridPane.columnIndex="0" GridPane.rowIndex="0">
<graphic>
<MaterialDesignIconView glyphName="BOOK_OPEN_VARIANT" size="24" />
</graphic>
</Button>
<Button contentDisplay="TOP" maxWidth="1.7976931348623157E308" text="New Script" GridPane.columnIndex="1" GridPane.rowIndex="0">
<Button contentDisplay="TOP" maxWidth="1.7976931348623157E308" onAction="#loadNewScript"
text="New Script" GridPane.columnIndex="1" GridPane.rowIndex="0">
<graphic>
<MaterialDesignIconView glyphName="NEW_BOX" size="24" />
</graphic>
......
......@@ -32,6 +32,35 @@ public class MatcherFacadeTest {
abbrev = new AbbrevMap();
}
@Test
public void matches() throws Exception {
shouldMatch("f(a)", "_");
shouldMatch("f(a)", "?X", "[{?X=f(a)}]");
shouldMatch("h(a,a)", "h(?X,?X)", "[{?X=a}]");
shouldMatch("h(a,b)", "h(?X,?X)", "[]");
//shouldMatch("f(a) ==> f(a), f(b)" , "==> f(?X)", [{?X=a}]);
//shouldMatch("f(a) ==> f(a), f(b)" , "f(a) ==> f(?X)", [{?X=a}]);
//shouldNotMatch("f(a) ==> f(a), f(b)" , "f(?X) ==> f(?X), f(a)");
//shouldMatch("f(a) ==> f(a), f(b)" , "==>");
//shouldMatch("f(a) ==> f(a), f(b)" , "_ ==> _");
//shouldMatch("f(a) ==> f(a), f(b)" , " ==> _");
//shouldMatch("f(a) ==> f(a), f(b)" , "_ ==> ");
}
private void shouldMatch(String key, String pattern) throws ParserException {
Term term = parseKeyTerm(key);
Matchings m = MatcherFacade.matches(pattern, term);
System.out.println(m);
}
private void shouldMatch(String key, String pattern, String exp) throws ParserException {
Term term = parseKeyTerm(key);
Matchings m = MatcherFacade.matches(pattern, term);
System.out.println(m);
Assert.assertEquals(exp, m.toString());
}
public Term parseKeyTerm(String term) throws ParserException {
Reader in = new StringReader(term);
......@@ -57,26 +86,4 @@ public class MatcherFacadeTest {
return dtp.parse(in, sort, services, namespace, abbrev);
}
@Test
public void matches() throws Exception {
shouldMatch("f(a)", "_");
shouldMatch("f(a)", "?X", "[{?X=f(a)}]");
shouldMatch("h(a,a)", "h(?X,?X)", "[{?X=a}]");
shouldMatch("h(a,b)", "h(?X,?X)", "[]");
}
private void shouldMatch(String key, String pattern, String exp) throws ParserException {
Term term = parseKeyTerm(key);
Matchings m = MatcherFacade.matches(pattern, term);
System.out.println(m);
Assert.assertEquals(exp, m.toString());
}
private void shouldMatch(String key, String pattern) throws ParserException {
Term term = parseKeyTerm(key);
Matchings m = MatcherFacade.matches(pattern, term);
System.out.println(m);
}
}
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment