Commit 27180e04 authored by Sarah Grebing's avatar Sarah Grebing
Browse files

settings now improtable

parent c822da5c
Pipeline #18174 failed with stages
in 84 minutes and 4 seconds
package edu.kit.iti.formal.psdbg.examples;
import de.uka.ilkd.key.proof.Proof;
import edu.kit.iti.formal.psdbg.gui.controller.DebuggerMain;
import javafx.beans.value.ChangeListener;
import javafx.beans.value.ObservableValue;
import org.apache.commons.io.IOUtils;
import java.io.File;
import java.io.IOException;
import java.io.*;
import java.net.URL;
import java.nio.charset.Charset;
......@@ -24,6 +26,12 @@ public class JavaExample extends Example {
protected URL javaFile;
protected URL settingsFile;
public void setSettingsFile(URL settingsFile) {
this.settingsFile = settingsFile;
}
@Override
public void open(DebuggerMain debuggerMain) {
//TODO should be reworked if we have an example
......@@ -39,7 +47,11 @@ public class JavaExample extends Example {
//System.out.println(java.getAbsolutePath());
//debuggerMain.openKeyFile(key);
debuggerMain.openJavaFile(java);
if (settingsFile != null) {
File settings = newTempFile(settingsFile, getName() + ".props");
ProofListener pl = new ProofListener(debuggerMain, settings);
debuggerMain.getFacade().proofProperty().addListener(pl);
}
debuggerMain.showActiveInspector(null);
if (helpText != null) {
String content = IOUtils.toString(helpText, Charset.defaultCharset());
......@@ -49,4 +61,31 @@ public class JavaExample extends Example {
e.printStackTrace();
}
}
public class ProofListener implements ChangeListener<Proof> {
File settingsFile;
DebuggerMain debuggerMain;
public ProofListener(DebuggerMain debuggerMain, File settingsFile) {
this.debuggerMain = debuggerMain;
this.settingsFile = settingsFile;
}
@Override
public void changed(ObservableValue<? extends Proof> observable, Proof oldValue, Proof newValue) {
if (newValue != null) {
try {
BufferedReader reader = new BufferedReader(new FileReader(settingsFile));
newValue.getSettings().loadSettingsFromStream(reader);
} catch (FileNotFoundException e) {
e.printStackTrace();
}
debuggerMain.getFacade().proofProperty().removeListener(this);
}
}
}
}
......@@ -8,16 +8,13 @@ public class QuickSort extends JavaExample {
setName("Quicksort example");
setSettingsFile(getClass().getResource("proof-settings.props"));
setHelpText(getClass().getResource("help.html"));
setJavaFile(getClass().
getResource("Quicksort.java"));
setScriptFile(getClass().
getResource("script.kps"));
setScriptFile(getClass().getResource("script.kps"));
}
}
......@@ -27,7 +27,7 @@ import java.util.Locale;
public class ProofScriptDebugger extends Application {
public static final String NAME = "Proof Script Debugger";
public static final String VERSION = "1.0.1e-FM";
public static final String VERSION = "1.0.2-FM";
public static final String KEY_VERSION = KeYConstants.VERSION;
......
......@@ -9,6 +9,7 @@ import de.uka.ilkd.key.logic.SequentFormula;
import de.uka.ilkd.key.macros.scripts.EngineState;
import de.uka.ilkd.key.macros.scripts.RuleCommand;
import de.uka.ilkd.key.macros.scripts.ScriptException;
import de.uka.ilkd.key.pp.LogicPrinter;
import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.proof.Proof;
......@@ -54,6 +55,7 @@ public class InteractiveModeController {
private static final Logger LOGGER = LogManager.getLogger(InteractiveModeController.class);
private final Map<Node, Statements> cases = new HashMap<>();
private final ScriptController scriptController;
private BooleanProperty activated = new SimpleBooleanProperty();
private ScriptArea scriptArea;
......@@ -72,6 +74,8 @@ public class InteractiveModeController {
private boolean moreThanOneMatch = false;
private CasesStatement casesStatement;
public void start(Proof currentProof, InspectionModel model) {
Events.register(this);
cases.clear();
......@@ -81,7 +85,17 @@ public class InteractiveModeController {
});
this.scriptArea = scriptController.newScript();
this.model = model;
casesStatement = new CasesStatement();
cases.forEach((k, v) -> {
val gcs = new GuardedCaseStatement();
val m = new MatchExpression();
m.setPattern(new StringLiteral(
format(LabelFactory.getBranchingLabel(k))
));
gcs.setGuard(m);
gcs.setBody(v);
casesStatement.getCases().add(gcs);
});
savepointslist = new ArrayList<>();
savepointsstatement = new ArrayList<>();
nodeAtInteractionStart = debuggerFramework.getStatePointer();
......@@ -136,30 +150,41 @@ public class InteractiveModeController {
Events.fire(new Events.InsertAtTheEndOfMainScript(c));
}
private String format(String branchingLabel) {
// System.out.println("branchingLabel = " + branchingLabel);
String newLabel = branchingLabel;
if (branchingLabel.endsWith("$$")) {
newLabel = branchingLabel.substring(0, branchingLabel.length() - 2);
newLabel += ".*";
// System.out.println("newLabel = " + newLabel);
}
return newLabel;
}
private Node findRoot(Node cur) {
while (cur != null) {
if (cases.keySet().contains(cur))
return cur;
cur = cur.parent();
}
return null;
}
@Subscribe
public void handle(Events.TacletApplicationEvent tap) {
LOGGER.debug("Handling {}", tap);
moreThanOneMatch = false;
String tapName = tap.getApp().taclet().displayName();
String tapName = tap.getApp().taclet().name().toString();
Goal g = tap.getCurrentGoal();
SequentFormula seqForm = tap.getPio().sequentFormula();
//transform term to parsable string representation
Sequent seq = g.sequent();
String sfTerm = edu.kit.iti.formal.psdbg.termmatcher.Utils.toPrettyTerm(seqForm.formula());
String onTerm = edu.kit.iti.formal.psdbg.termmatcher.Utils.toPrettyTerm(tap.getPio().subTerm());
//check whether more than one possibility for match
//Matchings matches = MatcherFacade.matches(term, seq, true, keYServices);
String sfTerm = LogicPrinter.quickPrintTerm(seqForm.formula(), keYServices, false, false);
String onTerm = LogicPrinter.quickPrintTerm(tap.getPio().subTerm(), keYServices, false, false);
/*Parameters params = new Parameters();
params.put(new Variable("formula"), new TermLiteral(term));
if (matches.size() > 1) {
moreThanOneMatch = true;
params.put(new Variable("occ"), new StringLiteral("0"));
}*/
RuleCommand.Parameters params = new RuleCommand.Parameters();
params.formula = seqForm.formula();
......@@ -170,7 +195,6 @@ public class InteractiveModeController {
int occ = rch.getOccurence(tap.getApp());
Parameters callp = new Parameters();
// callp.put(new Variable("formula"), new TermLiteral(sfTerm));
callp.put(new Variable("formula"), new TermLiteral(sfTerm));
callp.put(new Variable("occ"), new IntegerLiteral(BigInteger.valueOf(occ)));
callp.put(new Variable("on"), new TermLiteral(onTerm));
......@@ -191,8 +215,8 @@ public class InteractiveModeController {
applyRule(call, g);
// Insert into the right cases
Node currentNode = g.node();
cases.get(findRoot(currentNode)).add(call);
// Node currentNode = g.node();
// cases.get(findRoot(currentNode)).add(call);
// How to Play this on the Proof?
// How to Build a new StatePointer? Is it still possible?
......@@ -217,46 +241,6 @@ public class InteractiveModeController {
}
private Node findRoot(Node cur) {
while (cur != null) {
if (cases.keySet().contains(cur))
return cur;
cur = cur.parent();
}
return null;
}
public String getCasesAsString() {
CasesStatement c = new CasesStatement();
cases.forEach((k, v) -> {
val gcs = new GuardedCaseStatement();
val m = new MatchExpression();
m.setPattern(new StringLiteral(
format(LabelFactory.getBranchingLabel(k))
));
gcs.setGuard(m);
gcs.setBody(v);
c.getCases().add(gcs);
});
PrettyPrinter pp = new PrettyPrinter();
c.accept(pp);
return pp.toString();
}
private String format(String branchingLabel) {
System.out.println("branchingLabel = " + branchingLabel);
String newLabel = branchingLabel;
if (branchingLabel.endsWith("$$")) {
newLabel = branchingLabel.substring(0, branchingLabel.length() - 2);
newLabel += ".*";
System.out.println("newLabel = " + newLabel);
}
return newLabel;
}
private void applyRule(CallStatement call, Goal g) throws ScriptCommandNotApplicableException {
savepointslist.add(g.node());
savepointsstatement.add(call);
......@@ -289,21 +273,47 @@ public class InteractiveModeController {
map.put("#2", call.getCommand());
EngineState estate = new EngineState(g.proof());
estate.setGoal(g);
// System.out.println("on = " + map.get("on"));
// System.out.println("formula = " +map.get("formula"));
// System.out.println("occ = " + map.get("occ"));
//System.out.println("on = " + map.get("on"));
//System.out.println("formula = " + map.get("formula"));
//System.out.println("occ = " + map.get("occ"));
RuleCommand.Parameters cc = c.evaluateArguments(estate, map); //reflection exception
AbstractUserInterfaceControl uiControl = new DefaultUserInterfaceControl();
c.execute(uiControl, cc, estate);
ImmutableList<Goal> ngoals = g.proof().getSubtreeGoals(g.node());
ImmutableList<Goal> ngoals = g.proof().getSubtreeGoals(expandedNode.getData().getNode());
goals.remove(expandedNode);
GoalNode<KeyData> last = null;
for (Goal newGoalNode : ngoals) {
KeyData kdn = new KeyData(kd, newGoalNode.node());
goals.add(last = new GoalNode<>(expandedNode, kdn, kdn.getNode().isClosed()));
if (ngoals.size() > 1) {
cases.get(findRoot(ngoals.get(0).node())).add(call);
CasesStatement inner = new CasesStatement();
cases.get(findRoot(ngoals.get(0).node())).add(inner);
for (Goal newGoalNode : ngoals) {
KeyData kdn = new KeyData(kd, newGoalNode.node());
goals.add(last = new GoalNode<>(expandedNode, kdn, kdn.getNode().isClosed()));
val caseForSubNode = new GuardedCaseStatement();
val m = new MatchExpression();
m.setPattern(new StringLiteral(
format(LabelFactory.getBranchingLabel(newGoalNode.node()))
));
caseForSubNode.setGuard(m);
inner.getCases().add(caseForSubNode);
cases.put(last.getData().getNode(), caseForSubNode.getBody());
}
} else {
if (ngoals.size() == 0) {
cases.get(findRoot(expandedNode.getData().getNode())).add(call);
} else {
KeyData kdn = new KeyData(kd, ngoals.get(0).node());
goals.add(last = new GoalNode<>(expandedNode, kdn, kdn.getNode().isClosed()));
Node currentNode = last.getData().getNode();
cases.get(findRoot(currentNode)).add(call);
}
}
if (last != null)
model.setSelectedGoalNodeToShow(last);
......@@ -319,6 +329,12 @@ public class InteractiveModeController {
}
public String getCasesAsString() {
PrettyPrinter pp = new PrettyPrinter();
casesStatement.accept(pp);
return pp.toString();
}
public boolean isActivated() {
return activated.get();
}
......
......@@ -317,7 +317,7 @@ public class ScriptController {
lastScriptArea = area;
lastRegion = r;
} else {
logger.error("Could not find editor for the node to highlight: " + node.getOrigin());
logger.debug("Could not find editor for the node to highlight: " + node.getOrigin());
}
}
......
......@@ -298,8 +298,7 @@ public class Utils {
String msg = String.format("%s %d %s ", "There were still", noOfGoals,
"open goals.");
String msg2 = "You can continue the proof interactively by using the interactive button.\n" +
"This enables to point and click onto the sequents and apply rules\n"
+ "Applying splitting rules interactively is currently not supported yet.";
"This enables to point and click onto the sequents and apply rules.";
grid.add(new Label(msg), 0, 1);
grid.add(new MaterialDesignIconView(MaterialDesignIcon.HAND_POINTING_RIGHT, "24.0"), 3, 1);
......
#Proof-Settings-Config-File
#Mon Feb 05 16:31:07 CET 2018
[StrategyProperty]OSS_OPTIONS_KEY=OSS_ON
[StrategyProperty]VBT_PHASE=VBT_SYM_EX
[SMTSettings]useUninterpretedMultiplication=true
[SMTSettings]SelectedTaclets=
[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_CONTRACT
[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF
[StrategyProperty]SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY=SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER
[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_INVARIANT
[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF
[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF
[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS
[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_NONE
[SMTSettings]instantiateHierarchyAssumptions=true
[StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF
[StrategyProperty]DEP_OPTIONS_KEY=DEP_ON
[StrategyProperty]BLOCK_OPTIONS_KEY=BLOCK_CONTRACT
[StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_FREE
[StrategyProperty]SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY=SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF
[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_OFF
[Strategy]Timeout=-1
[Strategy]MaximumNumberOfAutomaticApplications=10000
[SMTSettings]integersMaximum=2147483645
[Choice]DefaultChoices=assertions-assertions\:safe , initialisation-initialisation\:disableStaticInitialisation , intRules-intRules\:arithmeticSemanticsIgnoringOF , programRules-programRules\:Java , runtimeExceptions-runtimeExceptions\:allow , JavaCard-JavaCard\:off , Strings-Strings\:on , modelFields-modelFields\:treatAsAxiom , bigint-bigint\:on , sequences-sequences\:on , moreSeqRules-moreSeqRules\:on , reach-reach\:on , integerSimplificationRules-integerSimplificationRules\:full , permissions-permissions\:off , wdOperator-wdOperator\:L , wdChecks-wdChecks\:off , mergeGenerateIsWeakeningGoal-mergeGenerateIsWeakeningGoal\:off
[SMTSettings]useConstantsForBigOrSmallIntegers=true
[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_ON
[StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE
[SMTSettings]maxGenericSorts=2
[SMTSettings]integersMinimum=-2147483645
[SMTSettings]invariantForall=false
[SMTSettings]UseBuiltUniqueness=false
[SMTSettings]explicitTypeHierarchy=false
[Strategy]ActiveStrategy=JavaCardDLStrategy
[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED
[StrategyProperty]MPS_OPTIONS_KEY=MPS_MERGE
......@@ -146,7 +146,7 @@ Your browser does not support the video tag or WebM.
</center>
Furthermore, we show how to use our SequentMatcher Window to enhance the auto-generated matching expressions from the
interactive rule applications. We are currently working on the support of interactively applying splitting rules and genearting the corresponding script.
interactive rule applications.
......@@ -208,18 +208,18 @@ interactive rule applications. We are currently working on the support of intera
<h2>Downloads</h2>
<ul>
<li>PSDBG - <strong>Version 1.0.1d-FM</strong>
<a href="../psdbg_releases/psdbg-1.0.1d-fm.jar">psdbg-1.0.1d-fm.jar</a>
<li>PSDBG - <strong>Version 1.0.2a-FM</strong>
<a href="../psdbg_releases/psdbg-1.0.2a-fm.jar">psdbg-1.0.2a-fm.jar</a>
<br>
Special Version for the tool paper at Formal Methods 2018.
Including examples and all dependencies.
<br>
Requires Java version 1.8.0_111 or higher; Not working with Java 9, because of depdendencies.
Requires Java version 1.8.0_111 or higher; Not working with Java 9, because of dependencies.
<br>
<a href="https://www.gnu.org/licenses/gpl-3.0.txt">License: GPLv3</a>
<a href="thirdparty.txt">Third Party Licenses</a>
<br>
Executable with <code>java -jar psdbg-1.0.1d-fm.jar</code>
Executable with <code>java -jar psdbg-1.0.2a-fm.jar</code>
</li>
</ul>
......
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