Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Spot
spins-ltsmin-deb
Commits
3c94f62c
Commit
3c94f62c
authored
Mar 31, 2016
by
Alfons Laarman
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Small refactor
parent
b543e6c6
Changes
16
Hide whitespace changes
Inline
Side-by-side
Showing
16 changed files
with
21 additions
and
67 deletions
+21
-67
src/spins/promela/compiler/actions/Action.java
src/spins/promela/compiler/actions/Action.java
+1
-1
src/spins/promela/compiler/actions/AssertAction.java
src/spins/promela/compiler/actions/AssertAction.java
+1
-1
src/spins/promela/compiler/actions/AssignAction.java
src/spins/promela/compiler/actions/AssignAction.java
+1
-1
src/spins/promela/compiler/actions/ChannelReadAction.java
src/spins/promela/compiler/actions/ChannelReadAction.java
+1
-1
src/spins/promela/compiler/actions/ChannelSendAction.java
src/spins/promela/compiler/actions/ChannelSendAction.java
+1
-1
src/spins/promela/compiler/actions/ExprAction.java
src/spins/promela/compiler/actions/ExprAction.java
+1
-1
src/spins/promela/compiler/actions/PrintAction.java
src/spins/promela/compiler/actions/PrintAction.java
+1
-1
src/spins/promela/compiler/automaton/ActionTransition.java
src/spins/promela/compiler/automaton/ActionTransition.java
+0
-8
src/spins/promela/compiler/automaton/ElseTransition.java
src/spins/promela/compiler/automaton/ElseTransition.java
+0
-16
src/spins/promela/compiler/automaton/EndTransition.java
src/spins/promela/compiler/automaton/EndTransition.java
+0
-16
src/spins/promela/compiler/automaton/Transition.java
src/spins/promela/compiler/automaton/Transition.java
+3
-15
src/spins/promela/compiler/automaton/UselessTransition.java
src/spins/promela/compiler/automaton/UselessTransition.java
+8
-0
src/spins/promela/compiler/ltsmin/LTSminTreeWalker.java
src/spins/promela/compiler/ltsmin/LTSminTreeWalker.java
+1
-1
src/spins/promela/compiler/ltsmin/model/LTSminTransition.java
...spins/promela/compiler/ltsmin/model/LTSminTransition.java
+1
-1
src/spins/promela/compiler/optimizer/RemoveUselessActions.java
...pins/promela/compiler/optimizer/RemoveUselessActions.java
+1
-2
src/spins/promela/compiler/optimizer/StateMerging.java
src/spins/promela/compiler/optimizer/StateMerging.java
+0
-1
No files found.
src/spins/promela/compiler/actions/Action.java
View file @
3c94f62c
...
...
@@ -37,7 +37,7 @@ public abstract class Action implements LTSminModelFeature {
}
public
boolean
isLocal
(
final
Proctype
proc
)
{
return
tru
e
;
return
fals
e
;
}
@Override
...
...
src/spins/promela/compiler/actions/AssertAction.java
View file @
3c94f62c
...
...
@@ -39,7 +39,7 @@ public class AssertAction extends Action {
return
false
;
}
}
return
super
.
isLocal
(
proc
)
;
return
true
;
}
@Override
...
...
src/spins/promela/compiler/actions/AssignAction.java
View file @
3c94f62c
...
...
@@ -49,7 +49,7 @@ public class AssignAction extends Action {
public
boolean
isLocal
(
final
Proctype
proc
)
{
if
(
expr
!=
null
&&
!(
new
ExprAction
(
expr
)).
isLocal
(
proc
))
return
false
;
return
proc
.
hasVariable
(
id
.
getVariable
().
getName
())
&&
super
.
isLocal
(
proc
)
;
return
proc
.
hasVariable
(
id
.
getVariable
().
getName
());
}
@Override
...
...
src/spins/promela/compiler/actions/ChannelReadAction.java
View file @
3c94f62c
...
...
@@ -74,7 +74,7 @@ public class ChannelReadAction extends Action implements CompoundExpression {
}
}
}
return
super
.
isLocal
(
proc
)
;
return
true
;
}
@Override
...
...
src/spins/promela/compiler/actions/ChannelSendAction.java
View file @
3c94f62c
...
...
@@ -74,7 +74,7 @@ public class ChannelSendAction extends Action implements CompoundExpression {
}
}
}
return
super
.
isLocal
(
proc
)
;
return
true
;
}
@Override
...
...
src/spins/promela/compiler/actions/ExprAction.java
View file @
3c94f62c
...
...
@@ -48,7 +48,7 @@ public class ExprAction extends Action {
}
if
(
null
!=
expr
.
getSideEffect
())
return
false
;
return
super
.
isLocal
(
proc
)
;
return
true
;
}
@Override
...
...
src/spins/promela/compiler/actions/PrintAction.java
View file @
3c94f62c
...
...
@@ -76,7 +76,7 @@ public class PrintAction extends Action implements CompoundExpression {
}
}
}
return
super
.
isLocal
(
proc
)
;
return
true
;
}
@Override
...
...
src/spins/promela/compiler/automaton/ActionTransition.java
View file @
3c94f62c
...
...
@@ -100,14 +100,6 @@ public class ActionTransition extends Transition {
return
true
;
}
/**
* @see spins.promela.compiler.automaton.Transition#isUseless()
*/
@Override
public
boolean
isUseless
()
{
return
false
;
}
/**
* @see spins.promela.compiler.automaton.Transition#getAction(int)
*/
...
...
src/spins/promela/compiler/automaton/ElseTransition.java
View file @
3c94f62c
...
...
@@ -42,22 +42,6 @@ public class ElseTransition extends Transition {
return
t
;
}
/**
* @see spins.promela.compiler.automaton.Transition#isLocal()
*/
@Override
public
boolean
isLocal
()
{
return
false
;
}
/**
* @see spins.promela.compiler.automaton.Transition#isUseless()
*/
@Override
public
boolean
isUseless
()
{
return
false
;
}
/**
* @see spins.promela.compiler.automaton.Transition#getText()
*/
...
...
src/spins/promela/compiler/automaton/EndTransition.java
View file @
3c94f62c
...
...
@@ -45,22 +45,6 @@ public class EndTransition extends Transition {
return
t
;
}
/**
* @see spins.promela.compiler.automaton.Transition#isLocal()
*/
@Override
public
boolean
isLocal
()
{
return
false
;
}
/**
* @see spins.promela.compiler.automaton.Transition#isUseless()
*/
@Override
public
boolean
isUseless
()
{
return
false
;
}
/**
* @see spins.promela.compiler.automaton.Transition#getText()
*/
...
...
src/spins/promela/compiler/automaton/Transition.java
View file @
3c94f62c
...
...
@@ -16,7 +16,6 @@ package spins.promela.compiler.automaton;
import
java.util.Collections
;
import
java.util.Iterator
;
import
java.util.List
;
import
spins.promela.compiler.Proctype
;
import
spins.promela.compiler.actions.Action
;
...
...
@@ -47,8 +46,6 @@ public abstract class Transition implements ActionContainer {
private
final
int
transId
;
private
List
<
String
>
labels
;
private
int
priority
=
-
1
;
protected
Transition
(
final
State
from
,
final
State
to
)
{
...
...
@@ -80,7 +77,6 @@ public abstract class Transition implements ActionContainer {
this
(
from
,
to
);
if
(
t
!=
null
)
{
this
.
priority
=
t
.
priority
;
this
.
labels
=
t
.
labels
;
}
}
...
...
@@ -288,7 +284,7 @@ public abstract class Transition implements ActionContainer {
getClass
().
getSimpleName
()).
append
(
" from "
).
append
(
from
==
null
?
"nowhere"
:
from
.
getStateId
()).
append
(
" to "
).
append
(
to
==
null
?
"nowhere"
:
to
.
getStateId
()).
append
(
" "
).
append
(
labels
==
null
?
""
:
" "
+
labels
).
append
(
getText
()).
toString
();
getText
()).
toString
();
}
public
boolean
isAlwaysEnabled
()
{
...
...
@@ -318,16 +314,8 @@ public abstract class Transition implements ActionContainer {
return
getFrom
().
getAutomaton
().
getProctype
();
}
public
void
setLabels
(
List
<
String
>
labels
)
{
this
.
labels
=
labels
;
}
public
List
<
String
>
getLabels
()
{
return
labels
;
}
public
int
getUnlessPriority
()
{
return
priority
;
public
int
getUnlessPriority
()
{
return
priority
;
}
public
void
setUnlessPriority
(
int
p
)
{
...
...
src/spins/promela/compiler/automaton/UselessTransition.java
View file @
3c94f62c
...
...
@@ -49,6 +49,14 @@ public class UselessTransition extends Transition {
return
t
;
}
/**
* @see spins.promela.compiler.automaton.Transition#isLocal()
*/
@Override
public
boolean
isLocal
()
{
return
true
;
}
/**
* @see spins.promela.compiler.automaton.Transition#isUseless()
*/
...
...
src/spins/promela/compiler/ltsmin/LTSminTreeWalker.java
View file @
3c94f62c
...
...
@@ -279,7 +279,7 @@ public class LTSminTreeWalker {
/* Statements are exported in SPIN format with line numbers for traces */
model
.
addType
(
STATEMENT_TYPE_NAME
);
model
.
addEdgeLabel
(
STATEMENT_EDGE_LABEL_NAME
,
STATEMENT_TYPE_NAME
);
for
(
LTSminTransition
t
:
model
.
getTransitions
())
{
for
(
LTSminTransition
t
:
model
.
getTransitions
())
{
Action
act
=
(
t
.
getTransition
().
getActionCount
()
>
0
?
t
.
getTransition
().
getAction
(
0
)
:
null
);
String
name
=
t
.
getName
().
split
(
"\t"
)[
1
];
int
line
=
null
==
act
?
-
1
:
act
.
getToken
().
beginLine
;
...
...
src/spins/promela/compiler/ltsmin/model/LTSminTransition.java
View file @
3c94f62c
...
...
@@ -266,7 +266,7 @@ public class LTSminTransition implements LTSminGuardContainer,
public
boolean
isProgress
()
{
return
begin
.
isProgress
()
||
State
.
hasLabelPrefix
(
original
.
getLabels
(),
State
.
LABEL_PROGRESS
);
State
.
hasLabelPrefix
(
original
.
getFrom
().
getLabels
(),
State
.
LABEL_PROGRESS
);
}
public
int
getIndex
()
{
...
...
src/spins/promela/compiler/optimizer/RemoveUselessActions.java
View file @
3c94f62c
...
...
@@ -33,9 +33,8 @@ public class RemoveUselessActions implements GraphOptimizer {
final
State
next
=
out
.
getTo
();
for
(
final
Transition
t
:
next
.
output
)
{
Transition
duplicate
=
t
.
duplicateFrom
(
state
);
t
.
duplicateFrom
(
state
);
//duplicate.changeFrom(state, out);
duplicate
.
setLabels
(
next
.
getLabels
());
}
uselessCount
++;
...
...
src/spins/promela/compiler/optimizer/StateMerging.java
View file @
3c94f62c
...
...
@@ -44,7 +44,6 @@ public class StateMerging implements GraphOptimizer {
for
(
final
Action
action
:
out
)
{
in
.
addAction
(
action
);
}
in
.
getFrom
().
addLabels
(
state
.
getLabels
());
state
.
delete
();
merged
++;
...
...
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