Commit 0430bb2f authored by Sarah Grebing's avatar Sarah Grebing

FM Version

parent a4d6ca6e
Pipeline #17205 failed with stages
in 83 minutes and 57 seconds
...@@ -136,7 +136,7 @@ public class DebuggerMain implements Initializable { ...@@ -136,7 +136,7 @@ public class DebuggerMain implements Initializable {
//----------------------------------------------------------------------------------------------------------------- //-----------------------------------------------------------------------------------------------------------------
private ProofTree proofTree = new ProofTree(); private ProofTree proofTree = new ProofTree();
private DockNode proofTreeDock = new DockNode(proofTree, "Proof Tree"); private DockNode proofTreeDock = new DockNode(proofTree, "Proof Tree");
private WelcomePane welcomePane = new WelcomePane(this); private WelcomePaneFMEdition welcomePane = new WelcomePaneFMEdition(this);
private DockNode welcomePaneDock = new DockNode(welcomePane, "Welcome", new MaterialDesignIconView(MaterialDesignIcon.ACCOUNT)); private DockNode welcomePaneDock = new DockNode(welcomePane, "Welcome", new MaterialDesignIconView(MaterialDesignIcon.ACCOUNT));
private DockNode activeInspectorDock; private DockNode activeInspectorDock;
private CommandHelp commandHelp = new CommandHelp(); private CommandHelp commandHelp = new CommandHelp();
...@@ -442,9 +442,8 @@ public class DebuggerMain implements Initializable { ...@@ -442,9 +442,8 @@ public class DebuggerMain implements Initializable {
// wait a second! // wait a second!
future.get(1, TimeUnit.SECONDS); future.get(1, TimeUnit.SECONDS);
// ungently stop // urgently stop
model.getDebuggerFramework().hardStop(); model.getDebuggerFramework().hardStop();
} catch (InterruptedException | ExecutionException | TimeoutException e) { } catch (InterruptedException | ExecutionException | TimeoutException e) {
e.printStackTrace(); e.printStackTrace();
} finally { } finally {
...@@ -453,6 +452,7 @@ public class DebuggerMain implements Initializable { ...@@ -453,6 +452,7 @@ public class DebuggerMain implements Initializable {
} else { } else {
LOGGER.info("no interpreter running"); LOGGER.info("no interpreter running");
} }
assert model.getDebuggerFramework() == null;
} }
@FXML @FXML
......
...@@ -17,6 +17,7 @@ import edu.kit.iti.formal.psdbg.gui.controls.ScriptArea; ...@@ -17,6 +17,7 @@ import edu.kit.iti.formal.psdbg.gui.controls.ScriptArea;
import edu.kit.iti.formal.psdbg.gui.controls.ScriptController; import edu.kit.iti.formal.psdbg.gui.controls.ScriptController;
import edu.kit.iti.formal.psdbg.gui.controls.Utils; import edu.kit.iti.formal.psdbg.gui.controls.Utils;
import edu.kit.iti.formal.psdbg.gui.model.InspectionModel; import edu.kit.iti.formal.psdbg.gui.model.InspectionModel;
import edu.kit.iti.formal.psdbg.interpreter.Evaluator;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode; import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData; import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment; import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
...@@ -25,6 +26,7 @@ import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode; ...@@ -25,6 +26,7 @@ import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode;
import edu.kit.iti.formal.psdbg.interpreter.exceptions.ScriptCommandNotApplicableException; import edu.kit.iti.formal.psdbg.interpreter.exceptions.ScriptCommandNotApplicableException;
import edu.kit.iti.formal.psdbg.parser.PrettyPrinter; import edu.kit.iti.formal.psdbg.parser.PrettyPrinter;
import edu.kit.iti.formal.psdbg.parser.ast.*; import edu.kit.iti.formal.psdbg.parser.ast.*;
import edu.kit.iti.formal.psdbg.parser.data.Value;
import edu.kit.iti.formal.psdbg.termmatcher.MatcherFacade; import edu.kit.iti.formal.psdbg.termmatcher.MatcherFacade;
import edu.kit.iti.formal.psdbg.termmatcher.Matchings; import edu.kit.iti.formal.psdbg.termmatcher.Matchings;
import javafx.beans.property.BooleanProperty; import javafx.beans.property.BooleanProperty;
...@@ -68,6 +70,8 @@ public class InteractiveModeController { ...@@ -68,6 +70,8 @@ public class InteractiveModeController {
private Proof currentProof; private Proof currentProof;
private Services keYServices; private Services keYServices;
private boolean moreThanOneMatch = false;
public void start(Proof currentProof, InspectionModel model) { public void start(Proof currentProof, InspectionModel model) {
Events.register(this); Events.register(this);
cases.clear(); cases.clear();
...@@ -134,7 +138,9 @@ public class InteractiveModeController { ...@@ -134,7 +138,9 @@ public class InteractiveModeController {
@Subscribe @Subscribe
public void handle(Events.TacletApplicationEvent tap) { public void handle(Events.TacletApplicationEvent tap) {
LOGGER.debug("Handling {}", tap); LOGGER.debug("Handling {}", tap);
moreThanOneMatch = false;
String tapName = tap.getApp().taclet().displayName(); String tapName = tap.getApp().taclet().displayName();
Goal g = tap.getCurrentGoal(); Goal g = tap.getCurrentGoal();
...@@ -147,18 +153,16 @@ public class InteractiveModeController { ...@@ -147,18 +153,16 @@ public class InteractiveModeController {
Parameters params = new Parameters(); Parameters params = new Parameters();
params.put(new Variable("formula"), new TermLiteral(term)); params.put(new Variable("formula"), new TermLiteral(term));
/* if(matches.size() > 1) { if (matches.size() > 1) {
System.out.println("matches = " + matches); moreThanOneMatch = true;
params.put(new Variable("occ"), new StringLiteral("0"));
Integer integ = new Integer(tap.getPio().sequentFormula().formula().serialNumber()); }
System.out.println("integ = " + integ);
params.put(new Variable("occ"), new IntegerLiteral(BigInteger.valueOf(integ)));
}*/
VariableAssignment va = new VariableAssignment(null); VariableAssignment va = new VariableAssignment(null);
CallStatement call = new CallStatement(tapName, params); CallStatement call = new CallStatement(tapName, params);
try { try {
applyRule(call, g); applyRule(call, g);
// Insert into the right cases // Insert into the right cases
Node currentNode = g.node(); Node currentNode = g.node();
...@@ -182,6 +186,7 @@ public class InteractiveModeController { ...@@ -182,6 +186,7 @@ public class InteractiveModeController {
} }
private Node findRoot(Node cur) { private Node findRoot(Node cur) {
while (cur != null) { while (cur != null) {
if (cases.keySet().contains(cur)) if (cases.keySet().contains(cur))
...@@ -237,8 +242,16 @@ public class InteractiveModeController { ...@@ -237,8 +242,16 @@ public class InteractiveModeController {
} }
RuleCommand c = new RuleCommand(); RuleCommand c = new RuleCommand();
// KeyData kd = g.getData(); // KeyData kd = g.getData();
Evaluator eval = new Evaluator(expandedNode.getAssignments(), expandedNode);
Map<String, String> map = new HashMap<>(); Map<String, String> map = new HashMap<>();
// call.getParameters().forEach((k, v) -> map.put(k.getIdentifier(), v.getData().toString())); call.getParameters().forEach((variable, expression) -> {
Value exp = eval.eval(expression);
map.put(variable.getIdentifier(), exp.getData().toString());
});
// call.getParameters().forEach((k, v) -> map.put(k.getIdentifier(),));
LOGGER.info("Execute {} with {}", call, map); LOGGER.info("Execute {} with {}", call, map);
try { try {
KeyData kd = expandedNode.getData(); KeyData kd = expandedNode.getData();
...@@ -246,6 +259,7 @@ public class InteractiveModeController { ...@@ -246,6 +259,7 @@ public class InteractiveModeController {
EngineState estate = new EngineState(g.proof()); EngineState estate = new EngineState(g.proof());
estate.setGoal(g); estate.setGoal(g);
RuleCommand.Parameters cc = c.evaluateArguments(estate, map); //reflection exception RuleCommand.Parameters cc = c.evaluateArguments(estate, map); //reflection exception
AbstractUserInterfaceControl uiControl = new DefaultUserInterfaceControl(); AbstractUserInterfaceControl uiControl = new DefaultUserInterfaceControl();
c.execute(uiControl, cc, estate); c.execute(uiControl, cc, estate);
...@@ -286,4 +300,6 @@ public class InteractiveModeController { ...@@ -286,4 +300,6 @@ public class InteractiveModeController {
public void setKeYServices(Services keYServices) { public void setKeYServices(Services keYServices) {
this.keYServices = keYServices; this.keYServices = keYServices;
} }
} }
...@@ -45,13 +45,18 @@ public class WelcomePaneFMEdition extends AnchorPane { ...@@ -45,13 +45,18 @@ public class WelcomePaneFMEdition extends AnchorPane {
* Load a test example * Load a test example
* @param event * @param event
*/ */
public void loadJavaTest(ActionEvent event) { public void loadQuicksort(ActionEvent event) {
proofScriptDebugger.getWelcomePaneDock().close(); proofScriptDebugger.getWelcomePaneDock().close();
proofScriptDebugger.showActiveInspector(null); proofScriptDebugger.showActiveInspector(null);
Examples.loadExamples().forEach(example -> {
if (example.getName().equals("Quicksort example")) {
example.open(proofScriptDebugger);
}
});
} }
/** /**
* Load teh help page documentation * Load the help page documentation
* @param event * @param event
*/ */
public void loadHelpPage(ActionEvent event) { public void loadHelpPage(ActionEvent event) {
......
edu.kit.iti.formal.psdbg.examples.contraposition.ContrapositionExample edu.kit.iti.formal.psdbg.examples.contraposition.ContrapositionExample
edu.kit.iti.formal.psdbg.examples.fol.FirstOrderLogicExample edu.kit.iti.formal.psdbg.examples.fol.FirstOrderLogicExample
edu.kit.iti.formal.psdbg.examples.java.simple.JavaSimpleExample
edu.kit.iti.formal.psdbg.examples.java.transitive.PaperExample
edu.kit.iti.formal.psdbg.examples.java.dpqs.DualPivotExample
edu.kit.iti.formal.psdbg.examples.java.quicksort.QuickSort edu.kit.iti.formal.psdbg.examples.java.quicksort.QuickSort
edu.kit.iti.formal.psdbg.examples.agatha.AgathaExample edu.kit.iti.formal.psdbg.examples.agatha.AgathaExample
edu.kit.iti.formal.psdbg.examples.java.bubbleSort.BubbleSortExample edu.kit.iti.formal.psdbg.examples.java.simple.JavaSimpleExample
edu.kit.iti.formal.psdbg.examples.java.sumAndMax.SumAndMaxExample
edu.kit.iti.formal.psdbg.examples.lulu.LuLuDoubleLinkedList
edu.kit.iti.formal.psdbg.examples.lulu.LuLuQuickSort
edu.kit.iti.formal.psdbg.examples.lulu.LuLuSumAndMax
...@@ -14,8 +14,8 @@ script split_from_quicksort() { ...@@ -14,8 +14,8 @@ script split_from_quicksort() {
case match `==> seqDef(_,_,_) = seqDef(_, _, _)`: case match `==> seqDef(_,_,_) = seqDef(_, _, _)`:
auto; auto;
case match `==> (\exists ?X (\exists ?Y _))`: case match `==> (\exists ?X (\exists ?Y _))`:
instantiate var=`?X`[?X \ X] with=`i_0`; instantiate var=X with=`i_0`;
instantiate var=`?Y`[?Y \ Y] with=`j_0`; instantiate var=Y with=`j_0`;
auto; auto;
} }
} }
......
...@@ -12,6 +12,6 @@ public class Test{ ...@@ -12,6 +12,6 @@ public class Test{
}else{ }else{
x++; x++;
} }
return x++; return ++x;
} }
} }
\ No newline at end of file
script t1(){ script t1(){
symbex; symbex;
cases{ foreach{
case match `?X >= 0,?X > 0 ==>`: onestep;
cut `?X = 0`[?X \ X]; andRight;
foreach{ foreach{
auto; tryclose;
} }
} }
// cases{
// case match `?X >= 0,?X > 0 ==>`:
// cut `?X = 0`[?X \ X];
// foreach{
// auto;
// }
// }
} }
...@@ -7,18 +7,23 @@ ...@@ -7,18 +7,23 @@
<?import javafx.scene.text.Font?> <?import javafx.scene.text.Font?>
<fx:root prefHeight="485.0" prefWidth="716.0" type="AnchorPane" xmlns="http://javafx.com/javafx/8.0.121" <fx:root prefHeight="485.0" prefWidth="716.0" type="AnchorPane" xmlns="http://javafx.com/javafx/8.0.121"
xmlns:fx="http://javafx.com/fxml/1"> xmlns:fx="http://javafx.com/fxml/1">
<children> <padding>
<Label layoutX="14.0" layoutY="14.0" text="Welcome to the ProofScriptDebugger"> <Insets top="25" right="25" bottom="25" left="25"/>
<font> </padding>
<Font size="24.0"/>
</font>
</Label>
<Label text="FM 2018 - Edition">
<font>
<Font size="20.0"/>
</font>
</Label>
<children>
<VBox>
<Label layoutX="14.0" layoutY="14.0" text="Welcome to the ProofScriptDebugger">
<font>
<Font size="24.0"/>
</font>
</Label>
<Label text="FM 2018 - Edition">
<font>
<Font size="20.0"/>
</font>
</Label>
</VBox>
<Label alignment="TOP_LEFT" layoutX="14.0" layoutY="71.0" prefHeight="129.0" prefWidth="573.0" <Label alignment="TOP_LEFT" layoutX="14.0" layoutY="71.0" prefHeight="129.0" prefWidth="573.0"
text="This application is the Proof Script debugger for the KeY system. It allows to perform proofs using a proof scripting language on top of the KeY system." text="This application is the Proof Script debugger for the KeY system. It allows to perform proofs using a proof scripting language on top of the KeY system."
wrapText="true"/> wrapText="true"/>
...@@ -99,8 +104,10 @@ ...@@ -99,8 +104,10 @@
</Button> </Button>
<!-- <Button contentDisplay="TOP" maxHeight="1.7976931348623157E308" maxWidth="1.7976931348623157E308" <Button contentDisplay="TOP" maxHeight="1.7976931348623157E308"
onAction="#loadJavaTest" text="Java Test Example" GridPane.columnIndex="1" GridPane.rowIndex="1"> maxWidth="1.7976931348623157E308"
onAction="#loadQuicksort" text="Quicksort Example" GridPane.columnIndex="1"
GridPane.rowIndex="1">
<graphic> <graphic>
<MaterialDesignIconView glyphName="NEW_BOX" size="24" /> <MaterialDesignIconView glyphName="NEW_BOX" size="24" />
</graphic> </graphic>
...@@ -113,7 +120,7 @@ ...@@ -113,7 +120,7 @@
<MaterialDesignIconView glyphName="NEW_BOX" size="24" /> <MaterialDesignIconView glyphName="NEW_BOX" size="24" />
</graphic> </graphic>
</Button> </Button>
-->
</children> </children>
<StackPane.margin> <StackPane.margin>
<Insets bottom="10.0" left="10.0" right="10.0" top="10.0"/> <Insets bottom="10.0" left="10.0" right="10.0" top="10.0"/>
......
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