Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in
Toggle navigation
Menu
Open sidebar
sarah.grebing
ProofScriptParser
Commits
69a12418
Commit
69a12418
authored
Jan 19, 2018
by
Sarah Grebing
Browse files
looking for regession
parent
15cc8d29
Pipeline
#17065
passed with stages
in 8 minutes and 54 seconds
Changes
3
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/ProofScriptCommandBuilder.java
View file @
69a12418
...
...
@@ -65,7 +65,7 @@ public class ProofScriptCommandBuilder implements CommandHandler<KeyData> {
KeyData
kd
=
expandedNode
.
getData
();
Map
<
String
,
String
>
map
=
new
HashMap
<>();
params
.
asMap
().
forEach
((
k
,
v
)
->
{
System
.
out
.
println
(
"v.getData().toString() = "
+
v
.
getData
().
toString
());
//
System.out.println("v.getData().toString() = " + v.getData().toString());
map
.
put
(
k
.
getIdentifier
(),
v
.
getData
().
toString
());
}
);
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/BaseCodeArea.java
View file @
69a12418
...
...
@@ -62,9 +62,14 @@ public class BaseCodeArea extends CodeArea {
}
protected
void
hightlightLine
(
LineMapping
lm
,
int
line
,
String
clazz
)
{
final
int
start
=
lm
.
getLineStart
(
line
);
final
int
end
=
lm
.
getLineEnd
(
line
);
setStyle
(
start
,
end
,
Collections
.
singleton
(
clazz
));
try
{
final
int
start
=
lm
.
getLineStart
(
line
);
final
int
end
=
lm
.
getLineEnd
(
line
);
setStyle
(
start
,
end
,
Collections
.
singleton
(
clazz
));
}
catch
(
ArrayIndexOutOfBoundsException
e
)
{
}
}
public
ObservableMap
<
Integer
,
String
>
getLineToClass
()
{
...
...
ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/quicksort/script.kps
View file @
69a12418
script split_from_quicksort
_nice1
() {
script split_from_quicksort() {
autopilot_prep;
foreach{
tryclose;
...
...
@@ -20,76 +20,3 @@ script split_from_quicksort_nice1() {
}
}
script split_from_quicksort_nice() {
autopilot_prep;
foreach{
tryclose;
}
foreach{
simp_upd;
seqPermFromSwap;
andRight;
}
cases{
case match `==> seqDef(_,_,_) = seqDef(_, _, _)`:
auto;
case match `==> \exists iv (\exists jv _)`: //this should match
instantiate var=`iv` with=`i_0`;
instantiate var=`jv` with=`j_0`;
auto;
}
}
script split_from_quicksort() {
autopilot_prep;
foreach{
tryclose;
}
cases{
default:
simp_upd; //only 2nd open goal needs this
seqPermFromSwap;
andRight;
}
cases{
case match '#0.*':
auto;
case match '#1.*':
instantiate var=`iv` with=`i_0`;
instantiate var=`jv` with=`j_0`;
auto;
}
}
script split_from_quicksort_rev() {
autopilot_prep;
foreach{
tryclose;
}
foreach{
simp_upd;
seqPermFromSwap;
andRight;
}
cases{
case match '#0.*': //hier sollten bessere branchnamen hin
auto;
case match '#1.*': //hier sollten bessere branchnamen hin
instantiate var=`iv` with=`i_0`;
instantiate var=`jv` with=`j_0`;
auto;
}
}
\ No newline at end of file
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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