diff --git a/lang/src/main/antlr4/edu/kit/iti/formal/psdbg/parser/ScriptLanguage.g4 b/lang/src/main/antlr4/edu/kit/iti/formal/psdbg/parser/ScriptLanguage.g4 index 193ace1c6b8637f9c01db33afcd32a9884ae55d7..53f8d0fbdc9f52dd418735a3c19eaabb9755d0f0 100644 --- a/lang/src/main/antlr4/edu/kit/iti/formal/psdbg/parser/ScriptLanguage.g4 +++ b/lang/src/main/antlr4/edu/kit/iti/formal/psdbg/parser/ScriptLanguage.g4 @@ -107,18 +107,18 @@ repeatStmt casesStmt : CASES INDENT casesList* - (DEFAULT COLON? INDENT + (DEFAULT COLON? INDENT? defList=stmtList - DEDENT)? + DEDENT?)? DEDENT ; casesList - : CASE (TRY | expression | closesExpression) COLON? INDENT stmtList DEDENT + : (TRY | CASE (expression | closesExpression)) COLON? INDENT? stmtList DEDENT? ; closesExpression - : CLOSES closesScript= scriptCommand + : CLOSES INDENT closesScript=stmtList DEDENT ; forEachStmt diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/TransformAst.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/TransformAst.java index 3ec9d809423d2e6b7182d740cedc61af4d86e55a..80bc662a29aef573bfc58defa1c123976fa285c4 100644 --- a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/TransformAst.java +++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/TransformAst.java @@ -328,7 +328,7 @@ public class TransformAst implements ScriptLanguageVisitor { ClosesCase closesCase = new ClosesCase(); closesCase.setClosedStmt(true); closesCase.setRuleContext(ctx); - closesCase.setClosesScript((CallStatement) ctx.closesExpression().closesScript.accept(this)); + closesCase.setClosesScript((Statements) ctx.closesExpression().closesScript.accept(this)); closesCase.setBody((Statements) ctx.stmtList().accept(this)); return closesCase; diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/ClosesCase.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/ClosesCase.java index c0a9cd893bb56e84ba539276e26702e7187cc94c..4c27c96e15e6b32a2e0845165b34b3da5e15e31a 100644 --- a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/ClosesCase.java +++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/ClosesCase.java @@ -16,7 +16,7 @@ public class ClosesCase extends CaseStatement { /** * Script that should be executed and shown whether case can be closed */ - private CallStatement closesScript; + private Statements closesScript; /** * A close subscript() {bodyscript} expression @@ -24,7 +24,7 @@ public class ClosesCase extends CaseStatement { * @param closesScript the script that is exectued in order to determine whether goal would clos. This proof is pruned afterwards * @param body the actual script that is then executed when closesscript was successful and pruned */ - public ClosesCase(CallStatement closesScript, Statements body) { + public ClosesCase(Statements closesScript, Statements body) { this.body = body; this.closesScript = closesScript; } @@ -41,8 +41,8 @@ public class ClosesCase extends CaseStatement { * {@inheritDoc} */ @Override - public tryCase copy() { - return new tryCase(body.copy()); + public ClosesCase copy() { + return new ClosesCase(closesScript.copy(), body.copy()); } } diff --git a/pom.xml b/pom.xml index 05d419bae402619f2730abb54217ea5a28dcbc84..bb7ebf92b2e2c0a3a7bbd8fa586d8f87c07d724d 100644 --- a/pom.xml +++ b/pom.xml @@ -57,7 +57,7 @@ rt rt-key ui - DockFX + lib/DockFX lint keydeps matcher diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/ProofScriptDebugger.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/ProofScriptDebugger.java index 89c353909854cdea354c6a735b7ffc96540771f9..28fc3fefb2015504dffe8c4985d3f8816413ddfb 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/ProofScriptDebugger.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/ProofScriptDebugger.java @@ -39,8 +39,11 @@ public class ProofScriptDebugger extends Application { Locale.setDefault(Locale.ENGLISH); try { - FXMLLoader fxmlLoader = new FXMLLoader(getClass().getResource( - "controller/DebuggerMain.fxml")); + +// FXMLLoader fxmlLoader = new FXMLLoader(getClass().getResource( +// "controller/DebuggerMain.fxml")); + FXMLLoader fxmlLoader = new FXMLLoader(getClass().getResource("/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.fxml")); + //"/edu/kit/formal/psdb/gui/controller/DebuggerMain.fxml")); Parent root = fxmlLoader.load(); //DebuggerMain controller = fxmlLoader.getController(); Scene scene = new Scene(root); diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/WelcomePane.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/WelcomePane.java index c5f5b5f5a024fecf37458653c6d0f0ad482bef01..be7b46bdb8df86ec92182913d6ef9fac37789256 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/WelcomePane.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/WelcomePane.java @@ -1,5 +1,6 @@ package edu.kit.iti.formal.psdbg.gui.controls; +import edu.kit.iti.formal.psdbg.examples.Examples; import edu.kit.iti.formal.psdbg.gui.controller.DebuggerMain; import javafx.event.ActionEvent; import javafx.scene.layout.AnchorPane; @@ -21,13 +22,19 @@ public class WelcomePane extends AnchorPane { public void loadContraPosition(ActionEvent event) { proofScriptDebugger.getWelcomePaneDock().close(); proofScriptDebugger.showActiveInspector(null); - proofScriptDebugger.openScript( - new File("src/test/resources/edu/kit/formal/psdb/interpreter/contraposition/w_branching.kps") + + Examples.loadExamples().forEach(example -> { + if (example.getName().equals("Contraposition")) + example.open(proofScriptDebugger); + + }); + /* proofScriptDebugger.openScript( + new File("") ); proofScriptDebugger.openKeyFile( new File("src/test/resources/edu/kit/formal/psdb/interpreter/contraposition/contraposition.key")); - + */ } public void loadJavaTest(ActionEvent event) { diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/help.html b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/help.html index 9ed114cfa2511748b5222dec38e3ab31b4923261..ba1aa8c708a9fbb26e53e8f7197689290b29bb13 100644 --- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/help.html +++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/help.html @@ -1,5 +1,8 @@

Contraposition

+

To load a script it needs to be called in the main script. + For example to load the script cpwob() type cpwob; in the body of the script main()

+ \ No newline at end of file diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps index dba523d56b11ac6d0a0cc408d5e963da89ae6005..956f1d4db1ef28b3e8db806352cbf61e4b07b8a2 100644 --- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps +++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps @@ -16,4 +16,36 @@ script cpwob () { replace_known_left occ='2'; concrete_impl_1; close; +} + +script cpwb () { + impRight; + impLeft; + cases{ + case match `==> p`:{ + auto; + } + default:{ + auto; + } + } +} + + +script cpClosable(){ + impRight; + impRight; + cases{ + case try:{ + notLeft; + notRight; + replace_known_left occ='2'; + concrete_impl_1; + close; + } + + default:{ + auto; + } + } } \ No newline at end of file