diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/ProofScriptCommandBuilder.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/ProofScriptCommandBuilder.java index 681e63a3f302fba2ff9252e968ade1655c656ab0..50bb3e2a0cc4a5ca668bda17fb3028192a29e2e9 100644 --- a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/ProofScriptCommandBuilder.java +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/ProofScriptCommandBuilder.java @@ -4,7 +4,6 @@ import de.uka.ilkd.key.control.AbstractUserInterfaceControl; import de.uka.ilkd.key.control.DefaultUserInterfaceControl; import de.uka.ilkd.key.macros.scripts.EngineState; import de.uka.ilkd.key.macros.scripts.ProofScriptCommand; -import de.uka.ilkd.key.macros.scripts.meta.ProofScriptArgument; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Node; import edu.kit.iti.formal.psdbg.interpreter.Interpreter; @@ -15,10 +14,14 @@ import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment; import edu.kit.iti.formal.psdbg.parser.ast.CallStatement; import lombok.Getter; import lombok.RequiredArgsConstructor; +import org.apache.commons.io.IOUtils; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; import org.key_project.util.collection.ImmutableList; +import java.io.IOException; +import java.net.URISyntaxException; +import java.net.URL; import java.util.Collection; import java.util.HashMap; import java.util.Iterator; @@ -104,17 +107,17 @@ public class ProofScriptCommandBuilder implements CommandHandler { @Override public String getHelp(CallStatement call) { ProofScriptCommand c = commands.get(call.getCommand()); - /* URL res = getClass().getResource("/edu/kit/iti/formal/psdbg/commands/" + call.getCommand() + ".html"); + URL res = getClass().getResource("/edu/kit/iti/formal/psdbg/commands/" + call.getCommand() + ".html"); try { return IOUtils.toString(res.toURI(), "utf-8"); } catch (NullPointerException | IOException | URISyntaxException e) { return "No Help found for " + call.getCommand(); - }*/ + } - StringBuilder html = new StringBuilder(); + /* StringBuilder html = new StringBuilder(); html.append(""); @@ -164,6 +167,6 @@ public class ProofScriptCommandBuilder implements CommandHandler { html.append(""); return html.toString(); - +*/ } } diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/RuleCommandHandler.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/RuleCommandHandler.java index 1251c96b0098e83c76a0e92b75a9395d193ed07f..c9c9bc7d9e028feac6817048c564154f0139f125 100644 --- a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/RuleCommandHandler.java +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/RuleCommandHandler.java @@ -41,6 +41,7 @@ import java.util.Set; */ @RequiredArgsConstructor public class RuleCommandHandler implements CommandHandler { + private static final Logger LOGGER = LogManager.getLogger(RuleCommandHandler.class); @Getter @@ -122,14 +123,17 @@ public class RuleCommandHandler implements CommandHandler { KeyData kdn = new KeyData(kd, g.node()); state.getGoals().add(new GoalNode<>(expandedNode, kdn, kdn.getNode().isClosed())); } - } catch (Exception e) { - if (e.getClass().equals(ScriptException.class)) { - System.out.println("e.getMessage() = " + e.getMessage()); + } catch (ScriptException e) { + if (interpreter.isStrictMode()) { throw new ScriptCommandNotApplicableException(e, c, map); - } else { - throw new RuntimeException(e); + //Utils necessary oder schmei├čen + LOGGER.error("Command " + call.getCommand() + " is not applicable in line " + call.getRuleContext().getStart().getLine()); } + } catch (InterruptedException e) { + e.printStackTrace(); + } catch (Exception e) { + e.printStackTrace(); } } diff --git a/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/rule.html b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/rule.html new file mode 100644 index 0000000000000000000000000000000000000000..96627cecdc862b02053b4a1e31fde096c241d4d1 --- /dev/null +++ b/rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/rule.html @@ -0,0 +1,21 @@ + + + + + rule + + +

Rule Application

+
+

Synopsis: rule tacletname on=<TERM> formula=<TERM> occ=<INT>

+
+Rule keyword can be ommited +

Arguments:

+
    +
  • rulename : STRING name of taclet to apply
  • +
  • on : TERM (find term of the taclet)
  • +
  • formula: TERM (top-level formula in which term appears)
  • +
  • occ : INT (occurrence number of term formula in sequent)
  • +
+ + diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java index 1145435f7ad2bfa35c05d7dcf22e1149e097fdc5..8223cf1dea2a2b0a4602802c7168f9d2ce6cfada 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java @@ -282,17 +282,15 @@ public class DebuggerMain implements Initializable { * @see {@link #handleStatePointer(PTreeNode)} */ private void handleStatePointerUI(PTreeNode node) { - - if (node != null) { - graph.addPartiallyAndMark(node); - getInspectionViewsController().getActiveInspectionViewTab().activate(node, node.getStateBeforeStmt()); scriptController.getDebugPositionHighlighter().highlight(node.getStatement()); } else { getInspectionViewsController().getActiveInspectionViewTab().getFrames().getItems().clear(); scriptController.getDebugPositionHighlighter().remove(); } + graph.addPartiallyAndMark(node); + } private void marriageJavaCode() { @@ -514,6 +512,7 @@ public class DebuggerMain implements Initializable { State lastState = statePointer.getStateAfterStmt(); getInspectionViewsController().getActiveInspectionViewTab().activate(statePointer, lastState); + }); } @@ -1008,7 +1007,7 @@ public class DebuggerMain implements Initializable { } } } else { - throw new RuntimeException("Something went wrong when reading stop button"); + throw new RuntimeException("Something went wrong when reloading"); } } @@ -1224,6 +1223,7 @@ public class DebuggerMain implements Initializable { ); node.dock(dockStation, DockPos.CENTER, scriptController.getOpenScripts().get(getScriptController().getMainScript().getScriptArea())); + node.requestFocus(); } } diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java index 00e9020fd2a1c803b397d939d558d92e13427f69..38d34cdca2ac7ccd9b52b324444d815a95c5de4f 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java @@ -312,7 +312,7 @@ public class ScriptController { getDockNode(area).focus(); area.requestFocus(); //area.scrollBy(new Point2D(0, scrollY)); - area.selectRange(0, r.start, 0, r.stop); + area.selectRange(0, r.start, 0, r.start); lastScriptArea = area; lastRegion = r; diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/Graph.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/Graph.java index c7d433f4c6e60e6904ce080ccb271eb070f4caf7..33e6672689fb2b27b6cac0224a1e226b6ec790bf 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/Graph.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/graph/Graph.java @@ -72,29 +72,33 @@ public class Graph { } public void addPartiallyAndMark(PTreeNode node) { - Cell cell = addCell(node); - - if (node.getStepOver() != null) { - addEdge(node, node.getStepOver(), "over"); - } - if (node.getStepInto() != null) { - addEdge(node, node.getStepInto(), "into"); - } - if (node.getStepInvOver() != null) { - addEdge(node, node.getStepInvOver(), "revo"); - } - if (node.getStepInvInto() != null) { - addEdge(node, node.getStepInvInto(), "otni"); - } - if (node.getStepReturn() != null) { - addEdge(node, node.getStepReturn(), "rtrn"); - } - if (lastHighlightedCell != null) { lastHighlightedCell.getStyleClass().remove("current-node"); } - cell.getStyleClass().add("current-node"); - lastHighlightedCell = cell; + + if (node != null) { + Cell cell = addCell(node); + + if (node.getStepOver() != null) { + addEdge(node, node.getStepOver(), "over"); + } + if (node.getStepInto() != null) { + addEdge(node, node.getStepInto(), "into"); + } + if (node.getStepInvOver() != null) { + addEdge(node, node.getStepInvOver(), "revo"); + } + if (node.getStepInvInto() != null) { + addEdge(node, node.getStepInvInto(), "otni"); + } + if (node.getStepReturn() != null) { + addEdge(node, node.getStepReturn(), "rtrn"); + } + + cell.getStyleClass().add("current-node"); + lastHighlightedCell = cell; + + } } } } diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/fol/script.kps b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/fol/script.kps index f7402d39e58651fcaec986fca0ecdd686e44ed09..199c22f5f618c112d890f914b7d4768957d39ec7 100644 --- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/fol/script.kps +++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/fol/script.kps @@ -1,10 +1,23 @@ // This file is not written yet!! + script main() { + feqff : TERM := `f(c) = f(f(c))`; + ffeqf : TERM := `f(f(c)) = f(c)`; + feqfff: TERM := `f(c) = f(f(f(c)))`; + + impRight; + instantiate var=`x` with=`c`; + applyEq on=`f(f(c))` formula=feqfff; + eqSymm on=feqff; + close; +} + +script main1() { impRight; //instantiate var=`x` with=`c`; //allLeft formula=`\forall` with=`a`; - allLeft on=`\forall s x; f(f(x)) = f(x)` inst_t=`c`; + //allLeft on=`\forall s x; f(f(x)) = f(x)` inst_t=`c`; }