Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
P
ProofScriptParser
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
24
Issues
24
List
Boards
Labels
Service Desk
Milestones
Merge Requests
4
Merge Requests
4
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Incidents
Environments
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
sarah.grebing
ProofScriptParser
Commits
418e70f7
Commit
418e70f7
authored
Apr 27, 2018
by
Sarah Grebing
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Cleaned Version for Website.
parent
957f9160
Pipeline
#21441
passed with stages
in 3 minutes and 22 seconds
Changes
9
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
9 changed files
with
93 additions
and
31 deletions
+93
-31
build.gradle
build.gradle
+1
-1
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/ProofScriptDebugger.java
...ava/edu/kit/iti/formal/psdbg/gui/ProofScriptDebugger.java
+1
-1
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentMatcher.java
...edu/kit/iti/formal/psdbg/gui/controls/SequentMatcher.java
+9
-2
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentOptionsMenu.java
...kit/iti/formal/psdbg/gui/controls/SequentOptionsMenu.java
+1
-0
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentViewForMatcher.java
.../iti/formal/psdbg/gui/controls/SequentViewForMatcher.java
+2
-0
ui/src/main/resources/META-INF/services/edu.kit.iti.formal.psdbg.examples.Example
...TA-INF/services/edu.kit.iti.formal.psdbg.examples.Example
+7
-7
ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps
...u/kit/iti/formal/psdbg/examples/contraposition/script.kps
+10
-20
ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script_for_Testing.kps
...rmal/psdbg/examples/contraposition/script_for_Testing.kps
+46
-0
website/docs/index.md
website/docs/index.md
+16
-0
No files found.
build.gradle
View file @
418e70f7
allprojects
{
apply
plugin:
'maven'
group
=
'edu.kit.iti.formal.psdbg'
version
=
'
1.0-FM
'
version
=
'
Experimental-1.1
'
}
subprojects
{
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/ProofScriptDebugger.java
View file @
418e70f7
...
...
@@ -29,7 +29,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-FM
"
;
public
static
final
String
VERSION
=
"
Experimental-1.1
"
;
public
static
final
String
KEY_VERSION
=
KeYConstants
.
VERSION
;
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentMatcher.java
View file @
418e70f7
...
...
@@ -25,6 +25,7 @@ import javafx.scene.control.ListView;
import
javafx.scene.control.TextArea
;
import
javafx.scene.input.MouseEvent
;
import
javafx.scene.layout.BorderPane
;
import
org.controlsfx.control.StatusBar
;
import
java.util.HashMap
;
import
java.util.Map
;
...
...
@@ -53,6 +54,7 @@ public class SequentMatcher extends BorderPane {
private
Label
nomatchings
;
//only shown when no matchings found, else always hidden
private
Map
<
PosInOccurrence
,
Range
>
cursorPosition
=
new
HashMap
<>();
public
SequentMatcher
(
Services
services
)
{
this
.
services
=
services
;
...
...
@@ -67,8 +69,13 @@ public class SequentMatcher extends BorderPane {
);
goalView
.
getSelectionModel
().
selectedItemProperty
().
addListener
((
prop
,
old
,
nnew
)
->
selectedGoalNodeToShow
.
setValue
(
nnew
)
);
{
if
(
nnew
!=
null
)
{
selectedGoalNodeToShow
.
setValue
(
nnew
);
}
else
{
selectedGoalNodeToShow
.
setValue
(
old
);
}
});
goalView
.
setCellFactory
(
GoalNodeListCell:
:
new
);
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentOptionsMenu.java
View file @
418e70f7
...
...
@@ -8,6 +8,7 @@ import javafx.fxml.FXML;
import
javafx.scene.Scene
;
import
javafx.scene.control.*
;
import
javafx.stage.Stage
;
import
org.controlsfx.control.StatusBar
;
public
class
SequentOptionsMenu
extends
ContextMenu
{
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentViewForMatcher.java
View file @
418e70f7
...
...
@@ -131,4 +131,6 @@ public class SequentViewForMatcher extends CodeArea {
public
LogicPrinter
.
PosTableStringBackend
getBackend
()
{
return
backend
;
}
}
ui/src/main/resources/META-INF/services/edu.kit.iti.formal.psdbg.examples.Example
View file @
418e70f7
edu.kit.iti.formal.psdbg.examples.contraposition.ContrapositionExample
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.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.agatha.AgathaExample
edu.kit.iti.formal.psdbg.examples.java.bubbleSort.BubbleSortExample
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
#
edu.kit.iti.formal.psdbg.examples.java.bubbleSort.BubbleSortExample
#
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
#edu.kit.iti.formal.psdbg.examples.lulu.bigIntProof.BigIntExample
\ No newline at end of file
ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps
View file @
418e70f7
// Please select one of the following scripts.
//
script testTry(){
cases{
try: impLeft;
default:
__KEY_MAX_STEPS:= 100;
impRight;
}
}
script testSMT(){
smt solver='Z3';
}
script toRemove(){
impRight;
useContract type='dependency' on=`p`;
}
script autoScript(){
__STRICT_MODE := true;
auto;
...
...
@@ -44,3 +24,13 @@ cases{
}
}
script usageOfTryInCases(){
cases{
try: impLeft; //if this mutator is successful, do this operation otherwise use next case
default:
__KEY_MAX_STEPS:= 100;
impRight;
}
}
\ No newline at end of file
ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script_for_Testing.kps
0 → 100644
View file @
418e70f7
// Please select one of the following scripts.
//
script testTry(){
cases{
try: impLeft;
default:
__KEY_MAX_STEPS:= 100;
impRight;
}
}
script testSMT(){
smt solver='Z3';
}
script toRemove(){
impRight;
useContract type='dependency' on=`p`;
}
script autoScript(){
__STRICT_MODE := true;
auto;
}
script interactive(){
impRight;
impRight;
impLeft;
}
script interactive_with_match(){
impRight;
impRight;
impLeft;
cases{
case match `==> !(?Z), ?Z`:
notRight;
default:
notLeft;
}
}
website/docs/index.md
View file @
418e70f7
...
...
@@ -209,6 +209,22 @@ interactive rule applications.
<h2>
Downloads
</h2>
<ul>
<li>
PSDBG -
<strong>
Experimental Version
</strong>
<a
href=
"../psdbg_releases/psdbg-Experimental-1.1.jar"
>
psdbg-Experimental-1.1.jar
</a>
<br>
This version is an experimental development version of PSDBG, including examples.
Its enhancements are based on an evaluation of the first version.
Not all provided features in this version may be completely functional yet.
<br>
One major change is the syntax for Matching Expressions. The wildcard symbol is now "?" instead of "_".
<br>
Requires Java version 1.8.0_111 or higher; Not working with Java 9, because of depdendencies.
<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-Experimental-1.1.jar
</code>
</li>
<li>
PSDBG -
<strong>
Version 1.0.2c-FM
</strong>
<a
href=
"../psdbg_releases/psdbg-1.0.2c-fm.jar"
>
psdbg-1.0.2c-fm.jar
</a>
<br>
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment