Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in
Toggle navigation
Menu
9.2.2023: Due to updates GitLab will be unavailable for some minutes between 9:00 and 11:00.
Open sidebar
i7
peregrine
Commits
4df80c03
Commit
4df80c03
authored
Aug 06, 2018
by
Philipp Meyer
Browse files
Rename initialPredicate to precondition
parent
c896169b
Changes
3
Hide whitespace changes
Inline
Side-by-side
src/Parser/PP.hs
View file @
4df80c03
...
...
@@ -175,7 +175,7 @@ data RecordPP = RecordPP {
transitions
::
[
RecordTransition
],
initialStates
::
[
String
],
trueStates
::
[
String
],
initialPredicate
::
Maybe
(
Formula
String
),
precondition
::
Maybe
(
Formula
String
),
predicate
::
Maybe
(
QuantFormula
String
),
description
::
Maybe
String
}
deriving
(
Show
)
...
...
@@ -185,14 +185,14 @@ $(deriveJSON defaultOptions ''RecordPP)
recordPP2PopulationProtocol
::
RecordPP
->
PopulationProtocol
recordPP2PopulationProtocol
r
=
makePopulationProtocolFromStrings
(
title
r
)
(
states
r
)
(
map
name
(
transitions
r
))
(
initialStates
r
)
(
trueStates
r
)
falseStates
p
i
p
arcs
where
makePopulationProtocolFromStrings
(
title
r
)
(
states
r
)
(
map
name
(
transitions
r
))
(
initialStates
r
)
(
trueStates
r
)
falseStates
p
p
recond
arcs
where
falseStates
=
[
q
|
q
<-
states
r
,
not
(
S
.
member
q
(
S
.
fromList
(
trueStates
r
)))]
arcs
=
[(
q
,
name
t
,
1
)
|
t
<-
transitions
r
,
q
<-
pre
t
]
++
[(
name
t
,
q
,
1
)
|
t
<-
transitions
r
,
q
<-
post
t
]
p
=
case
predicate
r
of
Nothing
->
ExQuantFormula
[]
FTrue
(
Just
p'
)
->
p'
i
p
=
case
initialPredicate
r
of
Nothing
->
FTrue
(
Just
p'
)
->
p'
p
recond
=
case
precondition
r
of
Nothing
->
FTrue
(
Just
p'
)
->
p'
parseContent
::
Parser
PopulationProtocol
parseContent
=
do
...
...
src/PopulationProtocol.hs
View file @
4df80c03
...
...
@@ -6,7 +6,7 @@ module PopulationProtocol
Configuration
,
FlowVector
,
RConfiguration
,
RFlowVector
,
renameState
,
renameTransition
,
renameStatesAndTransitions
,
invertPopulationProtocol
,
name
,
showNetName
,
states
,
transitions
,
initialStates
,
trueStates
,
falseStates
,
predicate
,
initialPredicate
,
name
,
showNetName
,
states
,
transitions
,
initialStates
,
trueStates
,
falseStates
,
predicate
,
precondition
,
pre
,
lpre
,
post
,
lpost
,
mpre
,
mpost
,
context
,
makePopulationProtocol
,
makePopulationProtocolWithTrans
,
makePopulationProtocolFromStrings
,
makePopulationProtocolWithTransFromStrings
,
...
...
@@ -78,7 +78,7 @@ data PopulationProtocol = PopulationProtocol {
trueStates
::
[
State
],
falseStates
::
[
State
],
predicate
::
QuantFormula
State
,
initialPredicate
::
Formula
State
,
precondition
::
Formula
State
,
adjacencyQ
::
M
.
Map
State
([(
Transition
,
Integer
)],
[(
Transition
,
Integer
)]),
adjacencyT
::
M
.
Map
Transition
([(
State
,
Integer
)],
[(
State
,
Integer
)])
}
...
...
@@ -95,7 +95,7 @@ instance Show PopulationProtocol where
"
\n
True states : "
++
show
(
trueStates
pp
)
++
"
\n
False states : "
++
show
(
falseStates
pp
)
++
"
\n
Predicate : "
++
show
(
predicate
pp
)
++
"
\n
Initial pred.
: "
++
show
(
initialPredicate
pp
)
++
"
\n
Precondition
: "
++
show
(
precondition
pp
)
++
"
\n
State arcs :
\n
"
++
unlines
(
map
showContext
(
M
.
toList
(
adjacencyQ
pp
)))
++
"
\n
Transition arcs:
\n
"
++
unlines
...
...
@@ -125,8 +125,8 @@ renameStatesAndTransitions f pp =
listSet
$
map
(
renameState
f
)
$
falseStates
pp
,
predicate
=
fmap
(
renameState
f
)
$
predicate
pp
,
initialPredicate
=
fmap
(
renameState
f
)
$
initialPredicate
pp
,
precondition
=
fmap
(
renameState
f
)
$
precondition
pp
,
adjacencyQ
=
mapAdjacency
(
renameState
f
)
(
renameTransition
f
)
$
adjacencyQ
pp
,
adjacencyT
=
mapAdjacency
(
renameTransition
f
)
(
renameState
f
)
$
...
...
@@ -146,7 +146,7 @@ invertPopulationProtocol pp =
trueStates
=
trueStates
pp
,
falseStates
=
falseStates
pp
,
predicate
=
predicate
pp
,
initialPredicate
=
initialPredicate
pp
,
precondition
=
precondition
pp
,
adjacencyQ
=
M
.
map
swap
$
adjacencyQ
pp
,
adjacencyT
=
M
.
map
swap
$
adjacencyT
pp
}
...
...
@@ -157,7 +157,7 @@ makePopulationProtocol :: String -> [State] -> [Transition] ->
[
State
]
->
[
State
]
->
[
State
]
->
QuantFormula
State
->
Formula
State
->
[
Either
(
Transition
,
State
,
Integer
)
(
State
,
Transition
,
Integer
)]
->
PopulationProtocol
makePopulationProtocol
name
states
transitions
initialStates
trueStates
falseStates
predicate
initialPredicate
arcs
=
makePopulationProtocol
name
states
transitions
initialStates
trueStates
falseStates
predicate
precondition
arcs
=
PopulationProtocol
{
name
=
name
,
states
=
listSet
states
,
...
...
@@ -166,7 +166,7 @@ makePopulationProtocol name states transitions initialStates trueStates falseSta
trueStates
=
listSet
trueStates
,
falseStates
=
listSet
falseStates
,
predicate
=
predicate
,
initialPredicate
=
initialPredicate
,
precondition
=
precondition
,
adjacencyQ
=
M
.
map
(
listMap
***
listMap
)
adQ
,
adjacencyT
=
M
.
map
(
listMap
***
listMap
)
adT
}
...
...
@@ -190,7 +190,7 @@ makePopulationProtocol name states transitions initialStates trueStates falseSta
makePopulationProtocolFromStrings
::
String
->
[
String
]
->
[
String
]
->
[
String
]
->
[
String
]
->
[
String
]
->
QuantFormula
String
->
Formula
String
->
[(
String
,
String
,
Integer
)]
->
PopulationProtocol
makePopulationProtocolFromStrings
name
states
transitions
initialStates
trueStates
falseStates
predicate
initialPredicate
arcs
=
makePopulationProtocolFromStrings
name
states
transitions
initialStates
trueStates
falseStates
predicate
precondition
arcs
=
makePopulationProtocol
name
(
map
State
(
S
.
toAscList
stateSet
))
...
...
@@ -199,7 +199,7 @@ makePopulationProtocolFromStrings name states transitions initialStates trueStat
(
map
State
trueStates
)
(
map
State
falseStates
)
(
fmap
State
predicate
)
(
fmap
State
initialPredicate
)
(
fmap
State
precondition
)
(
map
toEitherArc
arcs
)
where
stateSet
=
S
.
fromList
states
...
...
@@ -226,8 +226,8 @@ makePopulationProtocolFromStrings name states transitions initialStates trueStat
makePopulationProtocolWithTrans
::
String
->
[
State
]
->
[
State
]
->
[
State
]
->
[
State
]
->
QuantFormula
State
->
Formula
State
->
[(
Transition
,
([(
State
,
Integer
)],
[(
State
,
Integer
)]))]
->
PopulationProtocol
makePopulationProtocolWithTrans
name
states
initialStates
trueStates
falseStates
predicate
initialPredicate
ts
=
makePopulationProtocol
name
states
(
map
fst
ts
)
initialStates
trueStates
falseStates
predicate
initialPredicate
arcs
makePopulationProtocolWithTrans
name
states
initialStates
trueStates
falseStates
predicate
precondition
ts
=
makePopulationProtocol
name
states
(
map
fst
ts
)
initialStates
trueStates
falseStates
predicate
precondition
arcs
where
arcs
=
[
Right
(
q
,
t
,
w
)
|
(
t
,(
is
,
_
))
<-
ts
,
(
q
,
w
)
<-
is
]
++
[
Left
(
t
,
q
,
w
)
|
(
t
,(
_
,
os
))
<-
ts
,
(
q
,
w
)
<-
os
]
...
...
@@ -235,7 +235,7 @@ makePopulationProtocolWithTrans name states initialStates trueStates falseStates
makePopulationProtocolWithTransFromStrings
::
String
->
[
String
]
->
[
String
]
->
[
String
]
->
[
String
]
->
QuantFormula
String
->
Formula
String
->
[(
String
,
([(
String
,
Integer
)],
[(
String
,
Integer
)]))]
->
PopulationProtocol
makePopulationProtocolWithTransFromStrings
name
states
initialStates
trueStates
falseStates
predicate
initialPredicate
arcs
=
makePopulationProtocolWithTransFromStrings
name
states
initialStates
trueStates
falseStates
predicate
precondition
arcs
=
makePopulationProtocolWithTrans
name
(
map
State
states
)
...
...
@@ -243,7 +243,7 @@ makePopulationProtocolWithTransFromStrings name states initialStates trueStates
(
map
State
trueStates
)
(
map
State
falseStates
)
(
fmap
State
predicate
)
(
fmap
State
initialPredicate
)
(
fmap
State
precondition
)
(
map
toTArc
arcs
)
where
toTArc
(
t
,
(
iq
,
oq
))
=
...
...
src/Solver/StrongConsensus.hs
View file @
4df80c03
...
...
@@ -49,7 +49,7 @@ initialConfiguration :: PopulationProtocol -> SIMap State -> SBool
initialConfiguration
pp
m0
=
(
sum
(
mval
m0
(
initialStates
pp
))
.>=
2
)
&&&
(
sum
(
mval
m0
(
states
pp
\\
initialStates
pp
))
.==
0
)
&&&
(
evaluateFormula
(
initialPredicate
pp
)
m0
)
(
evaluateFormula
(
precondition
pp
)
m0
)
differentConsensusConstraints
::
Bool
->
PopulationProtocol
->
SIMap
State
->
SIMap
State
->
SIMap
State
->
SIMap
State
->
SIMap
State
->
SBool
differentConsensusConstraints
checkCorrectness
pp
m0
m1
m2
qe
qa
=
...
...
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