Skip to content
GitLab
Explore
Sign in
Commits on Source (3)
Fix parser
· d8aebc73
Philipp Meyer
authored
Aug 08, 2018
d8aebc73
Correctly use modulo predicates for checking correctness
· d3fec96f
Philipp Meyer
authored
Aug 08, 2018
d3fec96f
Update example remainder protocol with modulo usage
· 280b25b4
Philipp Meyer
authored
Aug 08, 2018
280b25b4
Show whitespace changes
Inline
Side-by-side
examples/remainder_m3_c1.pp
View file @
280b25b4
...
...
@@ -112,7 +112,7 @@
"_mod1"
,
"_mod2"
],
"predicate"
:
"
(
0 * _mod0 + 1 * _mod1 + 2 * _mod2
) % 3 =
1"
,
"predicate"
:
"0 * _mod0 + 1 * _mod1 + 2 * _mod2
=%3
1"
,
"trueStates"
:
[
"_mod1"
,
"_modpassivetrue"
...
...
src/Parser/PP.hs
View file @
280b25b4
...
...
@@ -103,6 +103,7 @@ parseOp = (reservedOp "<" *> return Lt) <|>
(
reservedOp
"="
*>
return
Eq
)
<|>
(
reservedOp
"!="
*>
return
Ne
)
<|>
(
reservedOp
">"
*>
return
Gt
)
<|>
(
reservedOp
">="
*>
return
Ge
)
<|>
(
reservedOp
"=%"
*>
(
ModEq
<$>
integer
))
<|>
(
reservedOp
"!=%"
*>
(
ModNe
<$>
integer
))
...
...
src/Property.hs
View file @
280b25b4
...
...
@@ -6,6 +6,8 @@ module Property
QuantFormula
(
..
),
quantifiedVariables
,
innerFormula
,
negationNormalForm
,
eliminateModulo
,
Op
(
..
),
Term
(
..
),
PropResult
(
..
),
...
...
@@ -89,8 +91,33 @@ negationNormalForm (Neg (FFalse)) = FTrue
negationNormalForm
(
Neg
(
g
:&:
h
))
=
(
negationNormalForm
(
Neg
g
))
:|:
(
negationNormalForm
(
Neg
h
))
negationNormalForm
(
Neg
(
g
:|:
h
))
=
(
negationNormalForm
(
Neg
g
))
:&:
(
negationNormalForm
(
Neg
h
))
negationNormalForm
(
Neg
(
LinearInequation
u
op
t
))
=
LinearInequation
u
(
negateOp
op
)
t
negationNormalForm
(
g
:&:
h
)
=
(
negationNormalForm
g
)
:&:
(
negationNormalForm
h
)
negationNormalForm
(
g
:|:
h
)
=
(
negationNormalForm
g
)
:|:
(
negationNormalForm
h
)
negationNormalForm
f
=
f
eliminateModulo
::
(
Int
->
a
)
->
Formula
a
->
(
Formula
a
,
[
a
])
eliminateModulo
=
eliminateModulo'
0
eliminateModulo'
::
Int
->
(
Int
->
a
)
->
Formula
a
->
(
Formula
a
,
[
a
])
eliminateModulo'
_
_
(
Neg
g
)
=
error
"Formula not in negation normal form: cannot eliminate modulo"
eliminateModulo'
n
makeVar
(
LinearInequation
lhs
(
ModEq
m
)
rhs
)
=
let
k
=
makeVar
n
in
(
LinearInequation
lhs
Eq
(
rhs
:+:
((
Const
m
)
:*:
(
Var
k
))),
[
k
])
eliminateModulo'
n
makeVar
(
LinearInequation
lhs
(
ModNe
m
)
rhs
)
=
let
j
=
makeVar
(
n
+
1
)
k
=
makeVar
n
in
((
LinearInequation
lhs
Eq
(
rhs
:+:
((
Var
j
)
:+:
((
Const
m
)
:*:
(
Var
k
)))))
:&:
(
LinearInequation
(
Const
0
)
Lt
(
Var
j
))
:&:
(
LinearInequation
(
Var
j
)
Lt
(
Const
m
)),
[
k
,
j
])
eliminateModulo'
n
makeVar
(
g
:|:
h
)
=
let
(
g'
,
ag
)
=
eliminateModulo'
n
makeVar
g
(
h'
,
ah
)
=
eliminateModulo'
(
n
+
length
ag
)
makeVar
h
in
(
g'
:|:
h'
,
ag
++
ah
)
eliminateModulo'
n
makeVar
(
g
:&:
h
)
=
let
(
g'
,
ag
)
=
eliminateModulo'
n
makeVar
g
(
h'
,
ah
)
=
eliminateModulo'
(
n
+
length
ag
)
makeVar
h
in
(
g'
:&:
h'
,
ag
++
ah
)
eliminateModulo'
_
_
f
=
(
f
,
[]
)
quantifiedVariables
::
QuantFormula
a
->
[
a
]
quantifiedVariables
(
ExQuantFormula
xs
_
)
=
xs
...
...
src/Solver/StrongConsensus.hs
View file @
280b25b4
...
...
@@ -21,6 +21,8 @@ import Property
import
Solver
import
Solver.Formula
import
Debug.Trace
type
StrongConsensusCounterExample
=
(
Configuration
,
Configuration
,
Configuration
,
FlowVector
,
FlowVector
)
type
StrongConsensusCompleteCounterExample
=
(
Configuration
,
Configuration
,
Configuration
,
FlowVector
,
FlowVector
,
Configuration
,
Configuration
,
Configuration
,
Configuration
)
type
RefinementObjects
=
([
Trap
],
[
Siphon
])
...
...
@@ -51,8 +53,9 @@ initialConfiguration pp m0 =
(
sum
(
mval
m0
(
states
pp
\\
initialStates
pp
))
.==
0
)
&&&
(
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
=
differentConsensusConstraints
::
Bool
->
PopulationProtocol
->
Formula
State
->
Formula
State
->
SIMap
State
->
SIMap
State
->
SIMap
State
->
SIMap
State
->
SIMap
State
->
SBool
differentConsensusConstraints
checkCorrectness
pp
pT
pF
m0
m1
m2
qe
qa
=
(
oT
&&&
oF
)
|||
(
if
checkCorrectness
then
correctnessConstraints
else
false
)
where
...
...
@@ -60,8 +63,9 @@ differentConsensusConstraints checkCorrectness pp m0 m1 m2 qe qa =
oF
=
sum
(
mval
m2
(
falseStates
pp
))
.>
0
correctnessConstraints
=
if
null
(
quantifiedVariables
(
predicate
pp
))
then
let
oP
=
evaluateFormula
(
innerFormula
(
predicate
pp
))
m0
in
(
oP
&&&
oF
)
|||
(
bnot
oP
&&&
oT
)
let
oPT
=
evaluateFormula
pT
(
M
.
union
m0
qe
)
oPF
=
evaluateFormula
pF
(
M
.
union
m0
qe
)
in
(
oPT
&&&
oF
)
|||
(
oPF
&&&
oT
)
else
let
oPT
=
evaluateFormula
(
innerFormula
(
predicate
pp
))
(
M
.
union
m0
qe
)
oPF
=
evaluateFormula
(
Neg
(
innerFormula
(
predicate
pp
)))
(
M
.
union
m0
qa
)
...
...
@@ -103,9 +107,10 @@ checkUSiphonConstraints :: PopulationProtocol -> SIMap State -> SIMap State -> S
checkUSiphonConstraints
pp
m0
m1
m2
x1
x2
siphons
=
bAnd
$
map
(
checkUSiphon
pp
m0
m1
m2
x1
x2
)
siphons
checkStrongConsensus
::
Bool
->
PopulationProtocol
->
SIMap
State
->
SIMap
State
->
SIMap
State
->
SIMap
Transition
->
SIMap
Transition
->
checkStrongConsensus
::
Bool
->
PopulationProtocol
->
Formula
State
->
Formula
State
->
SIMap
State
->
SIMap
State
->
SIMap
State
->
SIMap
Transition
->
SIMap
Transition
->
SIMap
State
->
SIMap
State
->
RefinementObjects
->
SBool
checkStrongConsensus
checkCorrectness
pp
m0
m1
m2
x1
x2
qe
qa
(
utraps
,
usiphons
)
=
checkStrongConsensus
checkCorrectness
pp
pT
pF
m0
m1
m2
x1
x2
qe
qa
(
utraps
,
usiphons
)
=
stateEquationConstraints
pp
m0
m1
x1
&&&
stateEquationConstraints
pp
m0
m2
x2
&&&
initialConfiguration
pp
m0
&&&
...
...
@@ -116,10 +121,19 @@ checkStrongConsensus checkCorrectness pp m0 m1 m2 x1 x2 qe qa (utraps, usiphons)
nonNegativityConstraints
x2
&&&
terminalConstraints
pp
m1
&&&
terminalConstraints
pp
m2
&&&
differentConsensusConstraints
checkCorrectness
pp
m0
m1
m2
qe
qa
&&&
differentConsensusConstraints
checkCorrectness
pp
pT
pF
m0
m1
m2
qe
qa
&&&
checkUTrapConstraints
pp
m0
m1
m2
x1
x2
utraps
&&&
checkUSiphonConstraints
pp
m0
m1
m2
x1
x2
usiphons
makePredicates
::
PopulationProtocol
->
(
Formula
State
,
Formula
State
,
[
State
])
makePredicates
pp
=
let
elim
s
f
=
eliminateModulo
(
State
.
(
s
++
)
.
show
)
f
fT
=
negationNormalForm
$
innerFormula
$
predicate
pp
fF
=
negationNormalForm
(
Neg
fT
)
(
pT
,
varsT
)
=
elim
"mpt'"
fT
(
pF
,
varsF
)
=
elim
"mpf'"
fF
in
(
pT
,
pF
,
varsT
++
varsF
)
checkStrongConsensusSat
::
Bool
->
PopulationProtocol
->
RefinementObjects
->
ConstraintProblem
Integer
StrongConsensusCounterExample
checkStrongConsensusSat
checkCorrectness
pp
refinements
=
let
m0
=
makeVarMapWith
(
"m0'"
++
)
$
states
pp
...
...
@@ -127,11 +141,12 @@ checkStrongConsensusSat checkCorrectness pp refinements =
m2
=
makeVarMapWith
(
"m2'"
++
)
$
states
pp
x1
=
makeVarMapWith
(
"x1'"
++
)
$
transitions
pp
x2
=
makeVarMapWith
(
"x2'"
++
)
$
transitions
pp
qe
=
makeVarMapWith
(
"e'"
++
)
$
quantifiedVariables
(
predicate
pp
)
(
pT
,
pF
,
modVars
)
=
makePredicates
pp
qe
=
makeVarMapWith
(
"e'"
++
)
$
modVars
qa
=
makeVarMapWith
(
"a'"
++
)
$
quantifiedVariables
(
predicate
pp
)
in
(
"strong consensus"
,
"(c0, c1, c2, x1, x2)"
,
getNames
m0
++
getNames
m1
++
getNames
m2
++
getNames
x1
++
getNames
x2
,
getNames
qe
,
getNames
qa
,
\
fm
->
checkStrongConsensus
checkCorrectness
pp
(
fmap
fm
m0
)
(
fmap
fm
m1
)
(
fmap
fm
m2
)
(
fmap
fm
x1
)
(
fmap
fm
x2
)
(
fmap
fm
qe
)
(
fmap
fm
qa
)
refinements
,
\
fm
->
checkStrongConsensus
checkCorrectness
pp
pT
pF
(
fmap
fm
m0
)
(
fmap
fm
m1
)
(
fmap
fm
m2
)
(
fmap
fm
x1
)
(
fmap
fm
x2
)
(
fmap
fm
qe
)
(
fmap
fm
qa
)
refinements
,
\
fm
->
counterExampleFromAssignment
(
fmap
fm
m0
)
(
fmap
fm
m1
)
(
fmap
fm
m2
)
(
fmap
fm
x1
)
(
fmap
fm
x2
))
counterExampleFromAssignment
::
IMap
State
->
IMap
State
->
IMap
State
->
IMap
Transition
->
IMap
Transition
->
StrongConsensusCounterExample
...
...
@@ -306,9 +321,10 @@ unusedBySequence pp max siphon x =
checkBounds
::
Integer
->
SIMap
State
->
SBool
checkBounds
max
=
bAnd
.
map
(
\
x
->
x
.>=
0
&&&
x
.<=
literal
max
)
.
vals
checkStrongConsensusComplete
::
Bool
->
PopulationProtocol
->
Integer
->
SIMap
State
->
SIMap
State
->
SIMap
State
->
SIMap
Transition
->
SIMap
Transition
->
checkStrongConsensusComplete
::
Bool
->
PopulationProtocol
->
Formula
State
->
Formula
State
->
Integer
->
SIMap
State
->
SIMap
State
->
SIMap
State
->
SIMap
Transition
->
SIMap
Transition
->
SIMap
State
->
SIMap
State
->
SIMap
State
->
SIMap
State
->
SIMap
State
->
SIMap
State
->
SBool
checkStrongConsensusComplete
checkCorrectness
pp
max
m0
m1
m2
x1
x2
r1
r2
s1
s2
qe
qa
=
checkStrongConsensusComplete
checkCorrectness
pp
pT
pF
max
m0
m1
m2
x1
x2
r1
r2
s1
s2
qe
qa
=
stateEquationConstraints
pp
m0
m1
x1
&&&
stateEquationConstraints
pp
m0
m2
x2
&&&
initialConfiguration
pp
m0
&&&
...
...
@@ -319,7 +335,7 @@ checkStrongConsensusComplete checkCorrectness pp max m0 m1 m2 x1 x2 r1 r2 s1 s2
nonNegativityConstraints
x2
&&&
terminalConstraints
pp
m1
&&&
terminalConstraints
pp
m2
&&&
differentConsensusConstraints
checkCorrectness
pp
m0
m1
m2
qe
qa
&&&
differentConsensusConstraints
checkCorrectness
pp
pT
pF
m0
m1
m2
qe
qa
&&&
checkBounds
max
r1
&&&
checkBounds
max
r2
&&&
checkBounds
max
s1
&&&
...
...
@@ -345,11 +361,12 @@ checkStrongConsensusCompleteSat checkCorrectness pp =
r2
=
makeVarMapWith
(
"r2'"
++
)
$
states
pp
s1
=
makeVarMapWith
(
"s1'"
++
)
$
states
pp
s2
=
makeVarMapWith
(
"s2'"
++
)
$
states
pp
qe
=
makeVarMapWith
(
"e'"
++
)
$
quantifiedVariables
(
predicate
pp
)
(
pT
,
pF
,
modVars
)
=
makePredicates
pp
qe
=
makeVarMapWith
(
"e'"
++
)
$
modVars
qa
=
makeVarMapWith
(
"a'"
++
)
$
quantifiedVariables
(
predicate
pp
)
in
(
"strong consensus"
,
"(m0, m1, m2, x1, x2, r1, r2, s1, s2)"
,
concatMap
getNames
[
m0
,
m1
,
m2
,
r1
,
r2
,
s1
,
s2
]
++
concatMap
getNames
[
x1
,
x2
],
getNames
qe
,
getNames
qa
,
\
fm
->
checkStrongConsensusComplete
checkCorrectness
pp
max
(
fmap
fm
m0
)
(
fmap
fm
m1
)
(
fmap
fm
m2
)
(
fmap
fm
x1
)
(
fmap
fm
x2
)
\
fm
->
checkStrongConsensusComplete
checkCorrectness
pp
pT
pF
max
(
fmap
fm
m0
)
(
fmap
fm
m1
)
(
fmap
fm
m2
)
(
fmap
fm
x1
)
(
fmap
fm
x2
)
(
fmap
fm
r1
)
(
fmap
fm
r2
)
(
fmap
fm
s1
)
(
fmap
fm
s2
)
(
fmap
fm
qe
)
(
fmap
fm
qa
),
\
fm
->
completeCounterExampleFromAssignment
max
(
fmap
fm
m0
)
(
fmap
fm
m1
)
(
fmap
fm
m2
)
(
fmap
fm
x1
)
(
fmap
fm
x2
)
(
fmap
fm
r1
)
(
fmap
fm
r2
)
(
fmap
fm
s1
)
(
fmap
fm
s2
))
...
...