Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
spins-ltsmin-deb
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
0
Issues
0
List
Boards
Labels
Service Desk
Milestones
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Incidents
Environments
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Spot
spins-ltsmin-deb
Commits
8e0eb28f
Commit
8e0eb28f
authored
Jan 14, 2018
by
Alfons Laarman
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Support structs in channels
parent
41d0d5a6
Changes
12
Hide whitespace changes
Inline
Side-by-side
Showing
12 changed files
with
292 additions
and
117 deletions
+292
-117
src/spins/promela/compiler/expression/Identifier.java
src/spins/promela/compiler/expression/Identifier.java
+6
-2
src/spins/promela/compiler/ltsmin/LTSminDMWalker.java
src/spins/promela/compiler/ltsmin/LTSminDMWalker.java
+27
-8
src/spins/promela/compiler/ltsmin/LTSminGMWalker.java
src/spins/promela/compiler/ltsmin/LTSminGMWalker.java
+36
-12
src/spins/promela/compiler/ltsmin/LTSminPrinter.java
src/spins/promela/compiler/ltsmin/LTSminPrinter.java
+99
-41
src/spins/promela/compiler/ltsmin/LTSminTreeWalker.java
src/spins/promela/compiler/ltsmin/LTSminTreeWalker.java
+79
-39
src/spins/promela/compiler/ltsmin/state/LTSminStateVector.java
...pins/promela/compiler/ltsmin/state/LTSminStateVector.java
+2
-2
src/spins/promela/compiler/ltsmin/state/LTSminSubVectorStruct.java
.../promela/compiler/ltsmin/state/LTSminSubVectorStruct.java
+3
-3
src/spins/promela/compiler/ltsmin/state/LTSminTypeChanStruct.java
...s/promela/compiler/ltsmin/state/LTSminTypeChanStruct.java
+7
-3
src/spins/promela/compiler/ltsmin/state/LTSminTypeStruct.java
...spins/promela/compiler/ltsmin/state/LTSminTypeStruct.java
+6
-0
src/spins/promela/compiler/ltsmin/util/CNF.java
src/spins/promela/compiler/ltsmin/util/CNF.java
+2
-1
src/spins/promela/compiler/ltsmin/util/LTSminUtil.java
src/spins/promela/compiler/ltsmin/util/LTSminUtil.java
+12
-0
src/spins/promela/compiler/ltsmin/util/SimplePredicate.java
src/spins/promela/compiler/ltsmin/util/SimplePredicate.java
+13
-6
No files found.
src/spins/promela/compiler/expression/Identifier.java
View file @
8e0eb28f
...
...
@@ -101,6 +101,10 @@ public class Identifier extends Expression {
this
.
sub
=
null
;
}
public
Identifier
(
Identifier
id
)
{
this
(
id
.
getToken
(),
id
.
var
,
id
.
getArrayExpr
(),
id
.
sub
);
}
public
Identifier
(
Identifier
id
,
Identifier
sub
)
{
this
(
id
.
getToken
(),
id
.
var
,
id
.
getArrayExpr
(),
sub
);
}
...
...
@@ -118,7 +122,7 @@ public class Identifier extends Expression {
*/
public
Expression
getArrayExpr
()
{
if
((
null
==
arrayExpr
)
!=
(-
1
==
var
.
getArraySize
()))
throw
new
AssertionError
(
"Invalid array semantics in expression: "
+
this
);
throw
new
AssertionError
(
"Invalid array semantics in expression: "
+
this
+
". Array size is: "
+
var
.
getArraySize
()
);
return
arrayExpr
;
}
...
...
@@ -187,7 +191,7 @@ public class Identifier extends Expression {
res
=
var
.
toString
()
+
"["
+
arrayExpr
.
toString
()
+
"]"
;
}
else
{
assert
(
false
);
res
=
var
.
toString
()
+
"[
0
]"
;
res
=
var
.
toString
()
+
"[
??
]"
;
}
}
else
{
res
=
var
.
toString
();
...
...
src/spins/promela/compiler/ltsmin/LTSminDMWalker.java
View file @
8e0eb28f
package
spins.promela.compiler.ltsmin
;
import
java.util.List
;
import
java.util.Map
;
import
static
spins
.
promela
.
compiler
.
Specification
.
_NR_PR
;
import
static
spins
.
promela
.
compiler
.
ltsmin
.
util
.
LTSminUtil
.
chanLength
;
import
static
spins
.
promela
.
compiler
.
ltsmin
.
util
.
LTSminUtil
.
channelBottom
;
import
static
spins
.
promela
.
compiler
.
ltsmin
.
util
.
LTSminUtil
.
channelIndex
;
import
static
spins
.
promela
.
compiler
.
ltsmin
.
util
.
LTSminUtil
.
channelNext
;
import
static
spins
.
promela
.
compiler
.
ltsmin
.
util
.
LTSminUtil
.
id
;
import
java.util.List
;
import
java.util.Map
;
import
spins.promela.compiler.Proctype
;
import
spins.promela.compiler.actions.Action
;
import
spins.promela.compiler.actions.AssertAction
;
...
...
@@ -57,6 +58,8 @@ import spins.promela.compiler.ltsmin.util.LTSminRendezVousException;
import
spins.promela.compiler.parser.ParseException
;
import
spins.promela.compiler.parser.PromelaConstants
;
import
spins.promela.compiler.variable.ChannelType
;
import
spins.promela.compiler.variable.ChannelVariable
;
import
spins.promela.compiler.variable.CustomVariableType
;
import
spins.promela.compiler.variable.Variable
;
import
spins.promela.compiler.variable.VariableType
;
...
...
@@ -102,11 +105,15 @@ public class LTSminDMWalker {
private
static
Params
sParams
=
new
Params
(
null
,
null
,
DUMMY_MATRIX
,
0
,
DUMMY_OPTIONS
);
public
static
void
walkOneGuard
(
LTSminModel
model
,
DepMatrix
dm
,
Expression
e
,
int
num
)
{
Expression
e
,
int
num
,
MarkAction
mark
)
{
sParams
.
model
=
model
;
sParams
.
depMatrix
.
read
=
dm
;
sParams
.
trans
=
num
;
walkExpression
(
sParams
,
e
,
MarkAction
.
READ
);
try
{
walkExpression
(
sParams
,
e
,
mark
);
}
catch
(
AssertionError
ae
)
{
throw
new
AssertionError
(
"Guard failed: "
+
e
+
"\n"
+
ae
);
}
}
static
void
walkModel
(
LTSminModel
model
,
LTSminDebug
debug
,
Options
opts
)
{
...
...
@@ -161,7 +168,7 @@ public class LTSminDMWalker {
report
.
setTotal
(
nLabels
*
nSlots
);
for
(
int
i
=
0
;
i
<
nLabels
;
i
++)
{
LTSminGuard
g
=
guardInfo
.
get
(
i
);
LTSminDMWalker
.
walkOneGuard
(
model
,
gm
,
g
.
expr
,
i
);
LTSminDMWalker
.
walkOneGuard
(
model
,
gm
,
g
.
expr
,
i
,
MarkAction
.
READ
);
reads
+=
gm
.
getRow
(
i
).
getCardinality
();
report
.
updateProgress
(
nSlots
);
}
...
...
@@ -222,7 +229,13 @@ public class LTSminDMWalker {
Params
p
=
new
Params
(
params
.
model
,
null
,
a2s
,
-
1
,
params
.
opts
);
for
(
Action
a
:
params
.
model
.
getActions
())
{
p
.
trans
=
a
.
getIndex
();
walkAction
(
p
,
a
);
try
{
walkAction
(
p
,
a
);
}
catch
(
AssertionError
ae
)
{
throw
new
AssertionError
(
"Walk Action failed: "
+
a
+
"\n"
+
ae
);
}
RWDepRow
row
=
a2s
.
getRow
(
a
.
getIndex
());
reads
+=
row
.
readCardinality
();
mayWrites
+=
row
.
mayWriteCardinality
();
...
...
@@ -524,13 +537,19 @@ public class LTSminDMWalker {
}
else
if
(
e
instanceof
ChannelReadExpression
)
{
ChannelReadExpression
cre
=
(
ChannelReadExpression
)
e
;
Identifier
id
=
cre
.
getIdentifier
();
ChannelVariable
cv
=
(
ChannelVariable
)
id
.
getVariable
();
ChannelType
ct
=
cv
.
getType
();
// mark variables as read
int
m
=
0
;
for
(
Expression
expr
:
cre
.
getExprs
())
{
Expression
read
=
cre
.
isRandom
()
?
channelIndex
(
id
,
STAR
,
m
)
:
channelBottom
(
id
,
m
);
walkExpression
(
params
,
read
,
mark
);
walkExpression
(
params
,
expr
,
mark
);
if
(
ct
.
getTypes
().
get
(
m
)
instanceof
CustomVariableType
)
{
walkExpression
(
params
,
expr
,
MarkAction
.
EREAD
);
}
else
{
walkExpression
(
params
,
expr
,
mark
);
}
m
++;
}
walkExpression
(
params
,
chanLength
(
id
),
mark
);
...
...
src/spins/promela/compiler/ltsmin/LTSminGMWalker.java
View file @
8e0eb28f
package
spins.promela.compiler.ltsmin
;
import
static
spins
.
promela
.
compiler
.
Specification
.
_NR_PR
;
import
static
spins
.
promela
.
compiler
.
ltsmin
.
LTSminPrinter
.
ICE_DM_NAME
;
import
static
spins
.
promela
.
compiler
.
ltsmin
.
LTSminPrinter
.
MDS_DM_NAME
;
import
static
spins
.
promela
.
compiler
.
ltsmin
.
LTSminPrinter
.
MES_DM_NAME
;
import
static
spins
.
promela
.
compiler
.
ltsmin
.
LTSminPrinter
.
ICE_DM_NAME
;
import
static
spins
.
promela
.
compiler
.
ltsmin
.
util
.
LTSminUtil
.
assign
;
import
static
spins
.
promela
.
compiler
.
ltsmin
.
util
.
LTSminUtil
.
chanLength
;
import
static
spins
.
promela
.
compiler
.
ltsmin
.
util
.
LTSminUtil
.
decr
;
...
...
@@ -36,6 +36,7 @@ import spins.promela.compiler.expression.Expression;
import
spins.promela.compiler.expression.Identifier
;
import
spins.promela.compiler.expression.RunExpression
;
import
spins.promela.compiler.expression.TimeoutExpression
;
import
spins.promela.compiler.ltsmin.LTSminDMWalker.MarkAction
;
import
spins.promela.compiler.ltsmin.LTSminTreeWalker.Options
;
import
spins.promela.compiler.ltsmin.matrix.DepMatrix
;
import
spins.promela.compiler.ltsmin.matrix.DepMatrix.DepRow
;
...
...
@@ -53,7 +54,10 @@ import spins.promela.compiler.ltsmin.util.SimplePredicate;
import
spins.promela.compiler.parser.ParseException
;
import
spins.promela.compiler.parser.PromelaTokenManager
;
import
spins.promela.compiler.variable.ChannelType
;
import
spins.promela.compiler.variable.ChannelVariable
;
import
spins.promela.compiler.variable.CustomVariableType
;
import
spins.promela.compiler.variable.Variable
;
import
spins.promela.compiler.variable.VariableType
;
/**
* A container for boolean state labels (part of which are guards), guard
...
...
@@ -471,7 +475,7 @@ guard_loop: for (int g2 : guardInfo.getTransMatrix().get(t2)) {
if
(
missed
)
{
RWMatrix
deps
=
model
.
getDepMatrix
();
DepMatrix
temp
=
new
DepMatrix
(
1
,
model
.
sv
.
size
());
LTSminDMWalker
.
walkOneGuard
(
model
,
temp
,
e
,
0
);
LTSminDMWalker
.
walkOneGuard
(
model
,
temp
,
e
,
0
,
MarkAction
.
READ
);
return
deps
.
getRow
(
t
.
getGroup
()).
mayWrites
(
temp
.
getRow
(
0
));
}
for
(
SimplePredicate
sp
:
sps
)
{
...
...
@@ -493,7 +497,7 @@ guard_loop: for (int g2 : guardInfo.getTransMatrix().get(t2)) {
for
(
Action
a
:
t
.
getActions
())
{
testSet
.
clear
();
LTSminDMWalker
.
walkOneGuard
(
model
,
testSet
,
sp
.
e
,
0
);
LTSminDMWalker
.
walkOneGuard
(
model
,
testSet
,
sp
.
e
,
0
,
MarkAction
.
READ
);
RWDepRow
writeSet
=
a2s
.
getRow
(
a
.
getIndex
());
if
(!
writeSet
.
mayWrites
(
testSet
.
getRow
(
0
)))
continue
;
...
...
@@ -590,7 +594,7 @@ guard_loop: for (int g2 : guardInfo.getTransMatrix().get(t2)) {
for
(
Action
a
:
t
.
getActions
())
{
testSet
.
clear
();
LTSminDMWalker
.
walkOneGuard
(
model
,
testSet
,
sp
.
e
,
0
);
LTSminDMWalker
.
walkOneGuard
(
model
,
testSet
,
sp
.
e
,
0
,
MarkAction
.
READ
);
RWDepRow
writeSet
=
a2s
.
getRow
(
a
.
getIndex
());
if
(!
writeSet
.
mayWrites
(
testSet
.
getRow
(
0
)))
continue
;
...
...
@@ -967,11 +971,20 @@ guard_loop: for (int g2 : guardInfo.getTransMatrix().get(t2)) {
throw
new
ParseException
();
}
else
if
(
a
instanceof
ChannelSendAction
)
{
ChannelSendAction
csa
=
(
ChannelSendAction
)
a
;
Identifier
id
=
csa
.
getIdentifier
();
Identifier
id
=
csa
.
getIdentifier
();
ChannelVariable
cv
=
(
ChannelVariable
)
id
.
getVariable
();
ChannelType
ct
=
cv
.
getType
();
int
m
=
0
;
for
(
Expression
e
:
csa
.
getExprs
())
{
if
(
depCheck
(
model
,
e
,
deps
.
mayWrite
))
throw
new
ParseException
();
VariableType
msg
=
ct
.
getTypes
().
get
(
m
++);
if
(
msg
instanceof
CustomVariableType
)
{
if
(
depCheck
(
model
,
e
,
deps
.
mayWrite
,
MarkAction
.
EREAD
))
throw
new
ParseException
();
}
else
{
if
(
depCheck
(
model
,
e
,
deps
.
mayWrite
))
throw
new
ParseException
();
}
}
if
(!
depCheck
(
model
,
chanLength
(
id
),
deps
))
...
...
@@ -988,11 +1001,22 @@ guard_loop: for (int g2 : guardInfo.getTransMatrix().get(t2)) {
}
else
if
(
a
instanceof
ChannelReadAction
)
{
ChannelReadAction
cra
=
(
ChannelReadAction
)
a
;
Identifier
id
=
cra
.
getIdentifier
();
ChannelVariable
cv
=
(
ChannelVariable
)
id
.
getVariable
();
ChannelType
ct
=
cv
.
getType
();
int
m
=
0
;
for
(
Expression
e
:
cra
.
getExprs
())
{
if
(
e
instanceof
Identifier
&&
depCheck
(
model
,
e
,
deps
))
throw
new
ParseException
();
m
++;
if
(!(
e
instanceof
Identifier
))
continue
;
VariableType
msg
=
ct
.
getTypes
().
get
(
m
-
1
);
if
(
msg
instanceof
CustomVariableType
)
{
if
(
depCheck
(
model
,
e
,
deps
,
MarkAction
.
EREAD
))
throw
new
ParseException
();
}
else
{
if
(
depCheck
(
model
,
e
,
deps
))
throw
new
ParseException
();
}
}
if
(!
depCheck
(
model
,
chanLength
(
id
),
deps
))
...
...
@@ -1154,7 +1178,7 @@ guard_loop: for (int g2 : guardInfo.getTransMatrix().get(t2)) {
DepRow
limit
=
limit1
!=
null
?
limit1
:
limit2
;
Expression
e
=
limit1
!=
null
?
e1
:
e2
;
DepMatrix
testSet
=
new
DepMatrix
(
1
,
model
.
sv
.
size
());
LTSminDMWalker
.
walkOneGuard
(
model
,
testSet
,
e
,
0
);
LTSminDMWalker
.
walkOneGuard
(
model
,
testSet
,
e
,
0
,
MarkAction
.
READ
);
if
(!
testSet
.
getRow
(
0
).
isDependent
(
limit
))
return
null
;
}
List
<
SimplePredicate
>
ga_sp
=
new
ArrayList
<
SimplePredicate
>();
...
...
src/spins/promela/compiler/ltsmin/LTSminPrinter.java
View file @
8e0eb28f
...
...
@@ -25,6 +25,7 @@ import static spins.promela.compiler.ltsmin.util.LTSminUtil.incr;
import
static
spins
.
promela
.
compiler
.
ltsmin
.
util
.
LTSminUtil
.
not
;
import
static
spins
.
promela
.
compiler
.
ltsmin
.
util
.
LTSminUtil
.
print
;
import
static
spins
.
promela
.
compiler
.
ltsmin
.
util
.
LTSminUtil
.
printPC
;
import
static
spins
.
promela
.
compiler
.
ltsmin
.
LTSminTreeWalker
.
createCustomIdentifiers
;
import
static
spins
.
promela
.
compiler
.
parser
.
PromelaConstants
.
ASSIGN
;
import
static
spins
.
promela
.
compiler
.
parser
.
PromelaConstants
.
DECR
;
import
static
spins
.
promela
.
compiler
.
parser
.
PromelaConstants
.
FALSE
;
...
...
@@ -94,7 +95,9 @@ import spins.promela.compiler.parser.ParseException;
import
spins.promela.compiler.parser.PromelaConstants
;
import
spins.promela.compiler.variable.ChannelType
;
import
spins.promela.compiler.variable.ChannelVariable
;
import
spins.promela.compiler.variable.CustomVariableType
;
import
spins.promela.compiler.variable.Variable
;
import
spins.promela.compiler.variable.VariableType
;
import
spins.util.IndexedSet
;
import
spins.util.StringWriter
;
...
...
@@ -525,8 +528,13 @@ public class LTSminPrinter {
w
.
appendPostfix
();
List
<
Action
>
actions
=
t
.
getActions
();
for
(
Action
a:
actions
)
generateAction
(
w
,
a
,
model
,
t
);
for
(
Action
a:
actions
)
{
try
{
generateAction
(
w
,
a
,
model
,
t
);
}
catch
(
AssertionError
ae
)
{
throw
new
AssertionError
(
"Generating action failed for "
+
a
+
"\n"
+
ae
);
}
}
// No edge labels! They are discarded anyway!
w
.
appendLine
(
"transition_info.group = "
+
t
.
getGroup
()
+
";"
);
if
(
t
.
getEnd
().
liesOnCycle
())
{
...
...
@@ -660,8 +668,13 @@ public class LTSminPrinter {
LTSminModel
model
)
{
w
.
appendLine
(
"memcpy("
,
OUT_VAR
,
", "
,
IN_VAR
,
", sizeof("
,
C_STATE
,
"));"
);
List
<
Action
>
actions
=
t
.
getActions
();
for
(
Action
a
:
actions
)
generateAction
(
w
,
a
,
model
,
t
);
for
(
Action
a
:
actions
)
{
try
{
generateAction
(
w
,
a
,
model
,
t
);
}
catch
(
AssertionError
ae
)
{
throw
ae
;
//new AssertionError("Generating action failed for "+ a +"\n"+ ae);
}
}
if
(
t
.
isAtomic
())
{
printEdgeLabels
(
w
,
model
,
t
);
w
.
appendLine
(
"transition_info.group = "
+
t
.
getGroup
()
+
";"
);
...
...
@@ -1045,36 +1058,44 @@ public class LTSminPrinter {
int
bufferSize
=
var
.
getType
().
getBufferSize
();
List
<
Expression
>
exprs
=
csa
.
getExprs
();
String
len
=
print
(
chanLength
(
id
),
out
(
model
));
ChannelVariable
cv
=
(
ChannelVariable
)
id
.
getVariable
();
ChannelType
ct
=
cv
.
getType
();
if
(
csa
.
isSorted
()
&&
bufferSize
>
1
)
{
Identifier
index
=
new
LTSminIdentifier
(
model
.
index
);
Expression
min
=
calc
(
PromelaConstants
.
MINUS
,
index
,
constant
(
1
));
Identifier
m0
=
channelIndex
(
id
,
min
,
0
);
Expression
comp
=
compare
(
PromelaConstants
.
LTE
,
m0
,
exprs
.
get
(
0
));
String
test
=
print
(
comp
,
out
(
model
));
w
.
appendLine
(
"for (i = "
+
len
+
"; i > 0; i--) {"
);
w
.
indent
();
w
.
appendLine
(
"if ("
+
test
+
") break;"
);
for
(
int
e
=
0
;
e
<
exprs
.
size
();
e
++)
{
Identifier
m
=
channelIndex
(
id
,
index
,
e
);
Identifier
mmm
=
channelIndex
(
id
,
min
,
e
);
generateAction
(
w
,
assign
(
m
,
mmm
),
model
,
t
);
}
w
.
outdent
();
w
.
appendLine
(
"}"
);
Identifier
index
=
new
LTSminIdentifier
(
model
.
index
);
Expression
min
=
calc
(
PromelaConstants
.
MINUS
,
index
,
constant
(
1
));
Identifier
m0
=
channelIndex
(
id
,
min
,
0
);
Expression
comp
=
compare
(
PromelaConstants
.
LTE
,
m0
,
exprs
.
get
(
0
));
String
test
=
print
(
comp
,
out
(
model
));
w
.
appendLine
(
"for (i = "
+
len
+
"; i > 0; i--) {"
);
w
.
indent
();
w
.
appendLine
(
"if ("
+
test
+
") break;"
);
for
(
int
e
=
0
;
e
<
exprs
.
size
();
e
++)
{
Identifier
m
=
channelIndex
(
id
,
index
,
e
);
Identifier
mmm
=
channelIndex
(
id
,
min
,
e
);
VariableType
msg
=
ct
.
getTypes
().
get
(
e
);
generateChanBufCopy
(
w
,
model
,
t
,
m
,
mmm
,
msg
);
//generateAction(w, assign(m, mmm), model, t);
}
w
.
outdent
();
w
.
appendLine
(
"}"
);
for
(
int
e
=
0
;
e
<
exprs
.
size
();
e
++)
{
final
Expression
expr
=
exprs
.
get
(
e
);
Identifier
buf
=
channelIndex
(
id
,
index
,
e
);
generateAction
(
w
,
assign
(
buf
,
expr
),
model
,
t
);
}
}
else
{
for
(
int
e
=
0
;
e
<
exprs
.
size
();
e
++)
{
final
Expression
expr
=
exprs
.
get
(
e
);
Identifier
buf
=
channelNext
(
id
,
e
);
generateAction
(
w
,
assign
(
buf
,
expr
),
model
,
t
);
}
for
(
int
e
=
0
;
e
<
exprs
.
size
();
e
++)
{
final
Expression
expr
=
exprs
.
get
(
e
);
Identifier
buf
=
channelIndex
(
id
,
index
,
e
);
VariableType
msg
=
ct
.
getTypes
().
get
(
e
);
generateChanBufCopy
(
w
,
model
,
t
,
buf
,
expr
,
msg
);
//generateAction(w, assign(buf, expr), model, t);
}
}
else
{
for
(
int
e
=
0
;
e
<
exprs
.
size
();
e
++)
{
final
Expression
expr
=
exprs
.
get
(
e
);
Identifier
buf
=
channelNext
(
id
,
e
);
VariableType
msg
=
ct
.
getTypes
().
get
(
e
);
generateChanBufCopy
(
w
,
model
,
t
,
buf
,
expr
,
msg
);
//generateAction(w, assign(buf, expr), model, t);
}
}
generateAction
(
w
,
incr
(
chanLength
(
id
)),
model
,
t
);
}
else
if
(
a
instanceof
ChannelReadAction
)
{
...
...
@@ -1098,14 +1119,18 @@ public class LTSminPrinter {
}
else
{
w
.
appendLine
(
"j = 0;"
);
}
for
(
int
e
=
0
;
e
<
exprs
.
size
();
e
++)
{
ChannelVariable
cv
=
(
ChannelVariable
)
id
.
getVariable
();
ChannelType
ct
=
cv
.
getType
();
for
(
int
e
=
0
;
e
<
exprs
.
size
();
e
++)
{
final
Expression
expr
=
exprs
.
get
(
e
);
if
(
expr
instanceof
Identifier
)
{
Identifier
p
=
(
Identifier
)
expr
;
Expression
m
=
channelBottom
(
id
,
e
);
generateAction
(
w
,
assign
(
p
,
m
),
model
,
t
);
}
if
(
!(
expr
instanceof
Identifier
))
continue
;
Identifier
lhs
=
(
Identifier
)
expr
;
Identifier
m
=
channelBottom
(
id
,
e
);
VariableType
msg
=
ct
.
getTypes
().
get
(
e
);
generateChanBufCopy
(
w
,
model
,
t
,
lhs
,
m
,
msg
);
}
if
(
cra
.
isRandom
())
{
w
.
appendLine
(
"break;"
);
w
.
outdent
();
...
...
@@ -1121,14 +1146,25 @@ public class LTSminPrinter {
for
(
int
e
=
0
;
e
<
exprs
.
size
();
e
++)
{
Identifier
m
=
channelIndex
(
id
,
index
,
e
);
Identifier
mpp
=
channelIndex
(
id
,
pp
,
e
);
generateAction
(
w
,
assign
(
m
,
mpp
),
model
,
t
);
VariableType
msg
=
ct
.
getTypes
().
get
(
e
);
generateChanBufCopy
(
w
,
model
,
t
,
m
,
mpp
,
msg
);
//generateAction(w, assign(m, mpp), model, t);
}
w
.
outdent
();
w
.
appendLine
(
"}"
);
}
generateAction
(
w
,
decr
(
chanLength
(
id
)),
model
,
t
);
for
(
int
e
=
0
;
e
<
exprs
.
size
();
e
++)
{
generateAction
(
w
,
assign
(
channelNext
(
id
,
e
),
constant
(
0
)),
model
,
t
);
VariableType
msg
=
ct
.
getTypes
().
get
(
e
);
Identifier
buf
=
channelNext
(
id
,
e
);
if
(
msg
instanceof
CustomVariableType
)
{
List
<
Identifier
>
l1
=
createCustomIdentifiers
(
msg
,
buf
);
for
(
Identifier
id1
:
l1
)
{
generateAction
(
w
,
assign
(
id1
,
constant
(
0
)),
model
,
t
);
}
}
else
{
generateAction
(
w
,
assign
(
buf
,
constant
(
0
)),
model
,
t
);
}
}
}
}
else
{
...
...
@@ -1136,11 +1172,27 @@ public class LTSminPrinter {
}
}
private
static
void
generateChanBufCopy
(
StringWriter
w
,
LTSminModel
model
,
LTSminTransition
t
,
Identifier
lhs
,
Expression
rhs
,
VariableType
msg
)
{
if
(
msg
instanceof
CustomVariableType
)
{
if
(!(
rhs
instanceof
Identifier
))
throw
new
AssertionError
(
"Expected identifier in rhs of channel XXX action buffer mod for: "
+
lhs
+
" := "
+
rhs
);
Identifier
R
=
(
Identifier
)
rhs
;
List
<
Identifier
>
l1
=
createCustomIdentifiers
(
msg
,
lhs
);
List
<
Identifier
>
l2
=
createCustomIdentifiers
(
msg
,
R
);
Iterator
<
Identifier
>
it2
=
l2
.
listIterator
();
for
(
Identifier
id1
:
l1
)
{
generateAction
(
w
,
assign
(
id1
,
it2
.
next
()),
model
,
t
);
}
}
else
{
generateAction
(
w
,
assign
(
lhs
,
rhs
),
model
,
t
);
}
}
private
static
void
copyAccess
(
LTSminModel
model
,
StringWriter
w
,
Identifier
id
)
{
if
(
id
.
getVariable
().
isHidden
()
||
id
instanceof
LTSminIdentifier
)
return
;
if
(
id
.
isConstant
())
return
;
String
var
=
print
(
id
,
out
(
model
));
String
var
=
print
(
id
,
out
(
model
));
if
(!
var
.
endsWith
(
".var"
))
throw
new
AssertionError
(
var
+
" does not end with '.var'"
);
String
pad
=
var
.
substring
(
0
,
var
.
length
()
-
4
)
+
".pad"
;
...
...
@@ -1199,7 +1251,13 @@ public class LTSminPrinter {
w
.
append
(
id
.
getVariable
().
getName
());
}
else
if
(
e
instanceof
Identifier
)
{
Identifier
id
=
(
Identifier
)
e
;
w
.
append
(
print
(
id
,
state
));
try
{
w
.
append
(
print
(
id
,
state
));
}
catch
(
AssertionError
ae
)
{
System
.
err
.
println
(
id
);
ae
.
printStackTrace
();
new
AssertionError
(
"Generating id failed for "
+
id
+
"\n"
+
ae
);
}
}
else
if
(
e
instanceof
AritmicExpression
)
{
AritmicExpression
ae
=
(
AritmicExpression
)
e
;
Expression
ex1
=
ae
.
getExpr1
();
...
...
src/spins/promela/compiler/ltsmin/LTSminTreeWalker.java
View file @
8e0eb28f
...
...
@@ -113,6 +113,7 @@ import spins.promela.compiler.parser.PromelaConstants;
import
spins.promela.compiler.parser.Token
;
import
spins.promela.compiler.variable.ChannelType
;
import
spins.promela.compiler.variable.ChannelVariable
;
import
spins.promela.compiler.variable.CustomVariableType
;
import
spins.promela.compiler.variable.Variable
;
import
spins.promela.compiler.variable.VariableType
;
...
...
@@ -147,10 +148,10 @@ public class LTSminTreeWalker {
private
void
replaceVars
(
Variable
v
,
Identifier
id
)
{
for
(
Identifier
i
:
ids
)
{
if
(
i
.
getVariable
()
==
v
)
{
i
.
setVariable
(
id
.
getVariable
());
if
(
i
.
getArrayExpr
()
!=
null
)
throw
new
AssertionError
(
"Not a lhs var place holder: "
+
i
+
" = "
+
id
);
i
.
setArrayIndex
(
id
.
getArrayExpr
());
i
.
setVariable
(
id
.
getVariable
());
}
}
}
...
...
@@ -1475,51 +1476,90 @@ public class LTSminTreeWalker {
// create transitions for all items in a channel array
for
(
int
x
=
0
;
x
<
(
arraySize
==
-
1
||
!
SPLIT
?
1
:
arraySize
);
x
++)
{
LTSminTransition
lt
=
new
LTSminTransition
(
sa
.
t
,
n
);
lt
.
setSync
(
ra
.
t
);
lt
.
addGuard
(
pcGuard
(
sa
.
t
.
getFrom
(),
sa
.
p
));
lt
.
addGuard
(
pcGuard
(
ra
.
t
.
getFrom
(),
ra
.
p
));
addSpecialGuards
(
lt
,
sa
.
t
,
sa
.
p
);
// proc die order && provided condition
addSpecialGuards
(
lt
,
ra
.
t
,
ra
.
p
);
// proc die order && provided condition
if
(
arraySize
>
-
1
)
{
// array of channels
if
(
SPLIT
)
lt
.
addGuard
(
compare
(
PromelaConstants
.
EQ
,
array1
,
constant
(
x
)));
lt
.
addGuard
(
compare
(
PromelaConstants
.
EQ
,
array1
,
array2
));
}
/* Channel matches */
for
(
int
i
=
0
;
i
<
cra_exprs
.
size
();
i
++)
{
final
Expression
csa_expr
=
csa_exprs
.
get
(
i
);
final
Expression
cra_expr
=
cra_exprs
.
get
(
i
);
if
(!(
cra_expr
instanceof
Identifier
))
{
lt
.
addGuard
(
compare
(
PromelaConstants
.
EQ
,
csa_expr
,
cra_expr
));
}
}
if
(
addNever
(
lt
,
n
))
{
set
.
add
(
lt
);
continue
;
}
lt
.
setSync
(
ra
.
t
);
lt
.
addGuard
(
pcGuard
(
sa
.
t
.
getFrom
(),
sa
.
p
));
lt
.
addGuard
(
pcGuard
(
ra
.
t
.
getFrom
(),
ra
.
p
));
addSpecialGuards
(
lt
,
sa
.
t
,
sa
.
p
);
// proc die order && provided condition
addSpecialGuards
(
lt
,
ra
.
t
,
ra
.
p
);
// proc die order && provided condition
if
(
arraySize
>
-
1
)
{
// array of channels
if
(
SPLIT
)
lt
.
addGuard
(
compare
(
PromelaConstants
.
EQ
,
array1
,
constant
(
x
)));
lt
.
addGuard
(
compare
(
PromelaConstants
.
EQ
,
array1
,
array2
));
}
/* Channel matches */
for
(
int
i
=
0
;
i
<
cra_exprs
.
size
();
i
++)
{
final
Expression
csa_expr
=
csa_exprs
.
get
(
i
);
final
Expression
cra_expr
=
cra_exprs
.
get
(
i
);
if
(!(
cra_expr
instanceof
Identifier
))
{
lt
.
addGuard
(
compare
(
PromelaConstants
.
EQ
,
csa_expr
,
cra_expr
));
}
}
if
(
addNever
(
lt
,
n
))
{
set
.
add
(
lt
);
continue
;
}
/* Channel reads */
for
(
int
i
=
0
;
i
<
cra_exprs
.
size
();
i
++)
{
final
Expression
csa_expr
=
csa_exprs
.
get
(
i
);
final
Expression
cra_expr
=
cra_exprs
.
get
(
i
);
if
(
cra_expr
instanceof
Identifier
)
{
lt
.
addAction
(
assign
((
Identifier
)
cra_expr
,
csa_expr
));
Identifier
id
=
cra
.
getIdentifier
();
ChannelVariable
cv
=
(
ChannelVariable
)
id
.
getVariable
();
ChannelType
ct
=
cv
.
getType
();
Identifier
cra_id
=
(
Identifier
)
cra_expr
;
VariableType
msg
=
ct
.
getTypes
().
get
(
i
);
if
(
msg
instanceof
CustomVariableType
)
{
if
(!(
csa_expr
instanceof
Identifier
))
throw
new
AssertionError
(
"Expected id in channel send action. "
+
cra
+
" index "
+
i
);
Identifier
csa_id
=
(
Identifier
)
csa_expr
;
List
<
Identifier
>
l1
=
createCustomIdentifiers
(
msg
,
csa_id
);
List
<
Identifier
>
l2
=
createCustomIdentifiers
(
msg
,
cra_id
);
Iterator
<
Identifier
>
it2
=
l2
.
listIterator
();
for
(
Identifier
id1
:
l1
)
{
lt
.
addAction
(
assign
(
it2
.
next
(),
id1
));
}
}
else
{
lt
.
addAction
(
assign
(
cra_id
,
csa_expr
));
}
}
}
// Change process counter of sender
lt
.
addAction
(
assign
(
sa
.
p
.
getPC
(),
sa
.
t
.
getTo
().
getStateId
()));
// Change process counter of receiver
lt
.
addAction
(
assign
(
ra
.
p
.
getPC
(),
ra
.
t
.
getTo
().
getStateId
()));
for
(
int
i
=
1
;
i
<
ra
.
t
.
getActionCount
();
i
++)
lt
.
addAction
(
ra
.
t
.
getAction
(
i
));
if
(
sa
.
t
.
getActionCount
()
>
1
)
throw
new
AssertionError
(
"Rendez-vous send action in d_step."
);
set
.
add
(
lt
);
// Change process counter of sender
lt
.
addAction
(
assign
(
sa
.
p
.
getPC
(),
sa
.
t
.
getTo
().
getStateId
()));
// Change process counter of receiver
lt
.
addAction
(
assign
(
ra
.
p
.
getPC
(),
ra
.
t
.
getTo
().
getStateId
()));
for
(
int
i
=
1
;
i
<
ra
.
t
.
getActionCount
();
i
++)
lt
.
addAction
(
ra
.
t
.
getAction
(
i
));
if
(
sa
.
t
.
getActionCount
()
>
1
)
throw
new
AssertionError
(
"Rendez-vous send action in d_step."
);