Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in
Toggle navigation
Menu
Open sidebar
i7
peregrine
Commits
6456c0fb
Commit
6456c0fb
authored
Dec 16, 2014
by
Philipp Meyer
Browse files
Parametrized formula, used reader monad and fixed types
parent
174936de
Changes
12
Hide whitespace changes
Inline
Side-by-side
src/Main.hs
View file @
6456c0fb
...
...
@@ -27,11 +27,11 @@ import Property
import
Structure
import
Solver
import
Solver.StateEquation
import
Solver.TrapConstraints
import
Solver.TransitionInvariant
import
Solver.LivenessInvariant
import
Solver.SComponent
import
Solver.CommFreeReachability
--
import Solver.TrapConstraints
--
import Solver.TransitionInvariant
--
import Solver.LivenessInvariant
--
import Solver.SComponent
--
import Solver.CommFreeReachability
data
InputFormat
=
PNET
|
LOLA
|
TPN
|
MIST
deriving
(
Show
,
Read
)
data
OutputFormat
=
OutLOLA
|
OutSARA
|
OutSPEC
|
OutDOT
deriving
(
Read
)
...
...
@@ -331,51 +331,51 @@ checkFile parser verbosity refine invariant implicitProperties transformations
verbosePut
verbosity
0
""
return
$
resultsAnd
rs
placeOp
::
Op
->
(
String
,
Integer
)
->
Formula
placeOp
op
(
p
,
w
)
=
Atom
$
LinIneq
(
Var
p
)
op
(
Const
w
)
placeOp
::
Op
->
(
Place
,
Integer
)
->
Formula
Place
placeOp
op
(
p
,
w
)
=
LinearInequation
(
Var
p
)
op
(
Const
w
)
transformNet
::
(
PetriNet
,
[
Property
])
->
NetTransformation
->
(
PetriNet
,
[
Property
])
transformNet
(
net
,
props
)
TerminationByReachability
=
let
ps
=
[
"'sigma"
,
"'m1"
,
"'m2"
]
++
places
net
++
map
prime
(
places
net
)
is
=
[(
"'m1"
,
1
)]
++
initials
net
++
map
(
first
prime
)
(
initials
net
)
let
m1
=
Place
"'m1"
m2
=
Place
"'m1"
sigma
=
Place
"'sigma"
switch
=
Transition
"'switch"
primePlace
=
renamePlace
prime
primeTransition
=
renameTransition
prime
ps
=
[
sigma
,
m1
,
m2
]
++
places
net
++
map
primePlace
(
places
net
)
is
=
[(
Place
"'m1"
,
1
)]
++
initials
net
++
map
(
first
primePlace
)
(
initials
net
)
transformTransition
t
=
let
(
preT
,
postT
)
=
context
net
t
pre'
=
[(
"'
m1
"
,
1
)]
++
preT
++
map
(
first
prime
)
preT
post'
=
[(
"'
m1
"
,
1
)]
++
postT
++
map
(
first
prime
)
postT
pre''
=
(
"'
m2
"
,
1
)
:
map
(
first
prime
)
preT
post''
=
[(
"'
m2
"
,
1
),
(
"'
sigma
"
,
1
)]
++
map
(
first
prime
)
postT
pre'
=
[(
m1
,
1
)]
++
preT
++
map
(
first
prime
Place
)
preT
post'
=
[(
m1
,
1
)]
++
postT
++
map
(
first
prime
Place
)
postT
pre''
=
(
m2
,
1
)
:
map
(
first
prime
Place
)
preT
post''
=
[(
m2
,
1
),
(
sigma
,
1
)]
++
map
(
first
prime
Place
)
postT
in
if
t
`
elem
`
ghostTransitions
net
then
[(
t
,
pre'
,
post'
)]
[(
t
,
(
pre'
,
post'
)
)
]
else
[(
t
,
pre'
,
post'
),
(
prime
t
,
pre''
,
post''
)]
ts
=
(
"'
switch
"
,
[(
"'
m1
"
,
1
)],
[(
"'
m2
"
,
1
)])
:
[(
t
,
(
pre'
,
post'
)
)
,
(
prime
Transition
t
,
(
pre''
,
post''
)
)
]
ts
=
(
switch
,
(
[(
m1
,
1
)],
[(
m2
,
1
)])
)
:
concatMap
transformTransition
(
transitions
net
)
gs
=
ghostTransitions
net
prop
=
Property
"termination by reachability"
$
Safety
$
foldl
(
:&:
)
(
Atom
(
LinIneq
(
Var
"'
sigma
"
)
Ge
(
Const
1
))
)
(
map
(
\
p
->
Atom
(
LinIneq
(
Var
(
prime
p
)
:-:
Var
p
)
Ge
(
Const
0
))
)
foldl
(
:&:
)
(
LinearInequation
(
Var
sigma
)
Ge
(
Const
1
))
(
map
(
\
p
->
LinearInequation
(
Var
(
prime
Place
p
)
:-:
Var
p
)
Ge
(
Const
0
))
(
places
net
))
-- TODO: map existing liveness properties
in
(
makePetriNetWith
Trans
(
name
net
)
ps
ts
is
gs
,
prop
:
props
)
in
(
makePetriNetWith
(
name
net
)
ps
ts
is
gs
,
prop
:
props
)
transformNet
(
net
,
props
)
ValidateIdentifiers
=
let
ps
=
map
validateId
$
places
net
ts
=
map
validateId
$
transitions
net
is
=
map
(
first
validateId
)
$
initials
net
as
=
map
(
\
(
a
,
b
,
x
)
->
(
validateId
a
,
validateId
b
,
x
))
$
arcs
net
gs
=
map
validateId
$
ghostTransitions
net
net'
=
makePetriNet
(
name
net
)
ps
ts
as
is
gs
props'
=
map
(
rename
validateId
)
props
in
(
net'
,
props'
)
(
renamePetriNetPlacesAndTransitions
validateId
net
,
map
(
renameProperty
validateId
)
props
)
makeImplicitProperty
::
PetriNet
->
ImplicitProperty
->
Property
makeImplicitProperty
net
Termination
=
Property
"termination"
$
Liveness
$
foldl
(
:&:
)
FTrue
(
map
(
\
t
->
Atom
(
LinIneq
(
Var
t
)
Eq
(
Const
0
))
)
(
map
(
\
t
->
LinearInequation
(
Var
t
)
Eq
(
Const
0
))
(
ghostTransitions
net
))
makeImplicitProperty
net
ProperTermination
=
let
(
finals
,
nonfinals
)
=
partition
(
null
.
lpost
net
)
(
places
net
)
...
...
@@ -423,8 +423,8 @@ checkProperty verbosity net refine invariant p = do
verbosePut
verbosity
3
$
show
p
r
<-
case
pcont
p
of
(
Safety
pf
)
->
checkSafetyProperty
verbosity
net
refine
invariant
pf
(
Liveness
pf
)
->
checkLivenessProperty
verbosity
net
refine
invariant
pf
(
Structural
ps
)
->
checkStructuralProperty
verbosity
net
ps
--
(Liveness pf) -> checkLivenessProperty verbosity net refine invariant pf
--
(Structural ps) -> checkStructuralProperty verbosity net ps
verbosePut
verbosity
0
$
showPropertyName
p
++
" "
++
case
r
of
Satisfied
->
"is satisfied."
...
...
@@ -433,20 +433,21 @@ checkProperty verbosity net refine invariant p = do
return
r
checkSafetyProperty
::
Int
->
PetriNet
->
Bool
->
Bool
->
Formula
->
IO
PropResult
Formula
Place
->
IO
PropResult
checkSafetyProperty
verbosity
net
refine
invariant
f
=
-- TODO: add flag for this kind of structural check
if
checkCommunicationFree
net
then
do
verbosePut
verbosity
1
"Net found to be communication-free"
checkSafetyPropertyByCommFree
verbosity
net
f
else
do
--if checkCommunicationFree net then do
-- verbosePut verbosity 1 "Net found to be communication-free"
-- checkSafetyPropertyByCommFree verbosity net f
--else
do
r
<-
checkSafetyPropertyBySafetyRef
verbosity
net
refine
f
[]
if
r
==
Satisfied
&&
invariant
then
-- TODO: add invariant generation
error
"Invariant generation for safety properties not yet supported"
else
return
r
{-
checkSafetyPropertyByCommFree :: Int -> PetriNet -> Formula -> IO PropResult
checkSafetyPropertyByCommFree verbosity net f = do
r <- checkSat $ checkCommFreeReachabilitySat net f
...
...
@@ -456,36 +457,33 @@ checkSafetyPropertyByCommFree verbosity net f = do
verbosePut verbosity 1 "Assignment found"
verbosePut verbosity 3 $ "Assignment: " ++ show a
return Unsatisfied
-}
checkSafetyPropertyBySafetyRef
::
Int
->
PetriNet
->
Bool
->
Formula
->
[[
String
]
]
->
IO
PropResult
Formula
Place
->
[
Trap
]
->
IO
PropResult
checkSafetyPropertyBySafetyRef
verbosity
net
refine
f
traps
=
do
r
<-
checkSat
$
checkStateEquationSat
net
f
traps
case
r
of
Nothing
->
return
Satisfied
Just
a
->
do
let
assigned
=
markedPlacesFromAssignment
net
a
Just
assigned
->
do
verbosePut
verbosity
1
"Assignment found"
verbosePut
verbosity
2
$
"Places marked: "
++
show
assigned
verbosePut
verbosity
3
$
"Assignment: "
++
show
a
if
refine
then
do
rt
<-
checkSat
$
checkTrapSat
net
assigned
rt
<-
return
Nothing
--
checkSat $ checkTrapSat net assigned
case
rt
of
Nothing
->
do
verbosePut
verbosity
1
"No trap found."
return
Unknown
Just
a
t
->
do
let
trap
=
trapFromAssignment
at
Just
t
rap
->
do
--
let trap = trapFromAssignment at
verbosePut
verbosity
1
"Trap found"
verbosePut
verbosity
2
$
"Places in trap: "
++
show
trap
verbosePut
verbosity
3
$
"Trap assignment: "
++
show
at
checkSafetyPropertyBySafetyRef
verbosity
net
refine
f
(
trap
:
traps
)
--verbosePut verbosity 2 $ "Places in trap: " ++
-- show trap
return
Unknown
--checkSafetyPropertyBySafetyRef verbosity net
-- refine f (trap:traps)
else
return
Unknown
{-
checkLivenessProperty :: Int -> PetriNet -> Bool -> Bool ->
Formula -> IO PropResult
checkLivenessProperty verbosity net refine invariant f = do
...
...
@@ -535,7 +533,7 @@ checkLivenessPropertyByRef verbosity net refine f comps = do
(sCompsCut:comps)
else
return (Unknown, comps)
-}
checkStructuralProperty
::
Int
->
PetriNet
->
Structure
->
IO
PropResult
checkStructuralProperty
_
net
struct
=
if
checkStructure
net
struct
then
...
...
src/Parser/LOLAFormula.hs
View file @
6456c0fb
...
...
@@ -48,20 +48,20 @@ binary name fun = Infix ( reservedOp name *> return fun )
prefix
::
String
->
(
a
->
a
)
->
Operator
String
()
Identity
a
prefix
name
fun
=
Prefix
(
reservedOp
name
*>
return
fun
)
termOperatorTable
::
[[
Operator
String
()
Identity
Term
]]
termOperatorTable
::
[[
Operator
String
()
Identity
(
Term
String
)
]]
termOperatorTable
=
[
[
prefix
"-"
Minus
]
,
[
binary
"*"
(
:*:
)
AssocLeft
]
,
[
binary
"+"
(
:+:
)
AssocLeft
,
binary
"-"
(
:-:
)
AssocLeft
]
]
termAtom
::
Parser
Term
termAtom
::
Parser
(
Term
String
)
termAtom
=
(
Var
<$>
identifier
)
<|>
(
Const
<$>
integer
)
<|>
parens
term
<?>
"basic term"
term
::
Parser
Term
term
::
Parser
(
Term
String
)
term
=
buildExpressionParser
termOperatorTable
termAtom
<?>
"term"
parseOp
::
Parser
Op
...
...
@@ -72,36 +72,36 @@ parseOp = (reservedOp "<" *> return Lt) <|>
(
reservedOp
">"
*>
return
Gt
)
<|>
(
reservedOp
">="
*>
return
Ge
)
linIneq
::
Parser
Formula
linIneq
::
Parser
(
Formula
String
)
linIneq
=
do
lhs
<-
term
op
<-
parseOp
rhs
<-
term
return
(
Atom
(
LinIneq
lhs
op
rhs
)
)
return
(
LinearInequation
lhs
op
rhs
)
binaryName
::
String
->
(
a
->
a
->
a
)
->
Assoc
->
Operator
String
()
Identity
a
binaryName
name
fun
=
Infix
(
reserved
name
*>
return
fun
)
prefixName
::
String
->
(
a
->
a
)
->
Operator
String
()
Identity
a
prefixName
name
fun
=
Prefix
(
reserved
name
*>
return
fun
)
formOperatorTable
::
[[
Operator
String
()
Identity
Formula
]]
formOperatorTable
::
[[
Operator
String
()
Identity
(
Formula
String
)
]]
formOperatorTable
=
[
[
prefixName
"NOT"
Neg
]
,
[
binaryName
"AND"
(
:&:
)
AssocRight
]
,
[
binaryName
"OR"
(
:|:
)
AssocRight
]
]
formAtom
::
Parser
Formula
formAtom
::
Parser
(
Formula
String
)
formAtom
=
try
linIneq
<|>
(
reserved
"TRUE"
*>
return
FTrue
)
<|>
(
reserved
"FALSE"
*>
return
FFalse
)
<|>
parens
formula
<?>
"basic formula"
formula
::
Parser
Formula
formula
::
Parser
(
Formula
String
)
formula
=
buildExpressionParser
formOperatorTable
formAtom
<?>
"formula"
parseFormula
::
Parser
Formula
parseFormula
::
Parser
(
Formula
String
)
parseFormula
=
do
whiteSpace
reserved
"FORMULA"
...
...
src/Parser/MIST.hs
View file @
6456c0fb
...
...
@@ -12,7 +12,7 @@ import Text.Parsec.Language (LanguageDef, emptyDef)
import
qualified
Text.Parsec.Token
as
Token
import
Parser
import
PetriNet
(
PetriNet
,
makePetriNetWithTrans
)
import
PetriNet
(
PetriNet
,
makePetriNetWithTrans
,
Place
(
..
)
)
import
Property
languageDef
::
LanguageDef
()
...
...
@@ -68,12 +68,12 @@ prop = do
return
$
Property
""
$
Safety
$
foldl1
(
:|:
)
$
map
(
foldl1
(
:&:
))
ineqs
ineq
::
Parser
Formula
ineq
::
Parser
(
Formula
Place
)
ineq
=
do
x
<-
identifier
reservedOp
">="
c
<-
integer
return
$
Atom
$
LinIneq
(
Var
x
)
Ge
(
Const
c
)
return
$
LinearInequation
(
Var
(
Place
x
)
)
Ge
(
Const
c
)
transitions
::
Parser
[(
String
,
[(
String
,
Integer
)],
[(
String
,
Integer
)])]
transitions
=
do
...
...
src/Parser/PNET.hs
View file @
6456c0fb
...
...
@@ -10,7 +10,7 @@ import Text.Parsec.Language (LanguageDef, emptyDef)
import
qualified
Text.Parsec.Token
as
Token
import
Parser
import
PetriNet
(
PetriNet
,
makePetriNet
)
import
PetriNet
(
PetriNet
,
makePetriNet
,
Place
(
..
),
Transition
(
..
)
)
import
Property
languageDef
::
LanguageDef
()
...
...
@@ -129,20 +129,20 @@ binary name fun = Infix ( reservedOp name *> return fun )
prefix
::
String
->
(
a
->
a
)
->
Operator
String
()
Identity
a
prefix
name
fun
=
Prefix
(
reservedOp
name
*>
return
fun
)
termOperatorTable
::
[[
Operator
String
()
Identity
Term
]]
termOperatorTable
::
[[
Operator
String
()
Identity
(
Term
String
)
]]
termOperatorTable
=
[
[
prefix
"-"
Minus
]
,
[
binary
"*"
(
:*:
)
AssocLeft
]
,
[
binary
"+"
(
:+:
)
AssocLeft
,
binary
"-"
(
:-:
)
AssocLeft
]
]
termAtom
::
Parser
Term
termAtom
::
Parser
(
Term
String
)
termAtom
=
(
Var
<$>
ident
)
<|>
(
Const
<$>
integer
)
<|>
parens
term
<?>
"basic term"
term
::
Parser
Term
term
::
Parser
(
Term
String
)
term
=
buildExpressionParser
termOperatorTable
termAtom
<?>
"term"
parseOp
::
Parser
Op
...
...
@@ -153,28 +153,28 @@ parseOp = (reservedOp "<" *> return Lt) <|>
(
reservedOp
">"
*>
return
Gt
)
<|>
(
reservedOp
">="
*>
return
Ge
)
linIneq
::
Parser
Formula
linIneq
::
Parser
(
Formula
String
)
linIneq
=
do
lhs
<-
term
op
<-
parseOp
rhs
<-
term
return
(
Atom
(
LinIneq
lhs
op
rhs
)
)
return
(
LinearInequation
lhs
op
rhs
)
formOperatorTable
::
[[
Operator
String
()
Identity
Formula
]]
formOperatorTable
::
[[
Operator
String
()
Identity
(
Formula
String
)
]]
formOperatorTable
=
[
[
prefix
"!"
Neg
]
,
[
binary
"&&"
(
:&:
)
AssocRight
]
,
[
binary
"||"
(
:|:
)
AssocRight
]
]
formAtom
::
Parser
Formula
formAtom
::
Parser
(
Formula
String
)
formAtom
=
try
linIneq
<|>
(
reserved
"true"
*>
return
FTrue
)
<|>
(
reserved
"false"
*>
return
FFalse
)
<|>
parens
formula
<?>
"basic formula"
formula
::
Parser
Formula
formula
::
Parser
(
Formula
String
)
formula
=
buildExpressionParser
formOperatorTable
formAtom
<?>
"formula"
propertyType
::
Parser
PropertyType
...
...
@@ -192,10 +192,11 @@ property = do
case
pt
of
SafetyType
->
do
form
<-
braces
formula
return
Property
{
pname
=
name
,
pcont
=
Safety
form
}
return
Property
{
pname
=
name
,
pcont
=
Safety
(
fmap
Place
form
)
}
LivenessType
->
do
form
<-
braces
formula
return
Property
{
pname
=
name
,
pcont
=
Liveness
form
}
return
Property
{
pname
=
name
,
pcont
=
Liveness
(
fmap
Transition
form
)
}
StructuralType
->
error
"structural property not supported for pnet"
parseContent
::
Parser
(
PetriNet
,[
Property
])
...
...
src/PetriNet.hs
View file @
6456c0fb
...
...
@@ -2,10 +2,11 @@
{-# OPTIONS_GHC -fno-warn-name-shadowing #-}
module
PetriNet
(
PetriNet
,
Place
,
Transition
,
Marking
,
tokens
,
buildMarking
,
(
PetriNet
,
Place
(
..
),
Transition
(
..
),
Marking
,
tokens
,
buildMarking
,
renamePlace
,
renameTransition
,
renamePetriNetPlacesAndTransitions
,
name
,
showNetName
,
places
,
transitions
,
initial
,
initialMarking
,
pre
,
lpre
,
post
,
lpost
,
initials
,
context
,
ghostTransitions
,
makePetriNet
,
makePetriNetWithTrans
)
makePetriNet
,
makePetriNetWithTrans
,
makePetriNetWith
)
where
import
qualified
Data.Map
as
M
...
...
@@ -85,21 +86,28 @@ instance Show PetriNet where
where
showContext
(
s
,(
l
,
r
))
=
show
l
++
" -> "
++
show
s
++
" -> "
++
show
r
--makePetriNet :: String -> [Place] -> [Transition] ->
-- [(Place, ([(Transition, Integer)], [(Transition, Integer)]))] ->
-- [(Transition, ([(Place, Integer)], [(Place, Integer)]))] ->
-- [(Place, Integer)] -> [Transition] -> PetriNet
--makePetriNet name places transitions placeArcs transitionArcs initial gs =
-- PetriNet { name=name, places=places, transitions=transitions,
-- adjacencyP=M.fromList (adjacencyFilter placeArcs),
-- adjacencyT=M.fromList (adjacencyFilter transitionArcs),
-- initialMarking=buildMarking initial,
-- ghostTransitions=gs }
-- where
-- adjacencyFilter = filter contextFilter
-- contextFilter (x,pre,post) =
-- (x,filter arcFilter pre, filter arcFilter post)
-- arcFilter (_,w) = w /= 0
renamePlace
::
(
String
->
String
)
->
Place
->
Place
renamePlace
f
(
Place
p
)
=
Place
(
f
p
)
renameTransition
::
(
String
->
String
)
->
Transition
->
Transition
renameTransition
f
(
Transition
t
)
=
Transition
(
f
t
)
renamePetriNetPlacesAndTransitions
::
(
String
->
String
)
->
PetriNet
->
PetriNet
renamePetriNetPlacesAndTransitions
f
net
=
PetriNet
{
name
=
name
net
,
places
=
map
(
renamePlace
f
)
$
places
net
,
transitions
=
map
(
renameTransition
f
)
$
transitions
net
,
adjacencyP
=
mapAdjacency
(
renamePlace
f
)
(
renameTransition
f
)
$
adjacencyP
net
,
adjacencyT
=
mapAdjacency
(
renameTransition
f
)
(
renamePlace
f
)
$
adjacencyT
net
,
initialMarking
=
Marking
$
M
.
mapKeys
(
renamePlace
f
)
$
getMarking
$
initialMarking
net
,
ghostTransitions
=
map
(
renameTransition
f
)
$
ghostTransitions
net
}
where
mapAdjacency
f
g
m
=
M
.
mapKeys
f
(
M
.
map
(
mapContext
g
)
m
)
mapContext
f
(
pre
,
post
)
=
(
map
(
first
f
)
pre
,
map
(
first
f
)
post
)
makePetriNet
::
String
->
[
String
]
->
[
String
]
->
[(
String
,
String
,
Integer
)]
->
...
...
@@ -134,6 +142,27 @@ makePetriNet name places transitions arcs initial gs =
" both places or transitions"
addArc
(
lNew
,
rNew
)
(
lOld
,
rOld
)
=
(
lNew
++
lOld
,
rNew
++
rOld
)
-- TODO: better constructors
makePetriNetWith
::
String
->
[
Place
]
->
[(
Transition
,
([(
Place
,
Integer
)],
[(
Place
,
Integer
)]))]
->
[(
Place
,
Integer
)]
->
[
Transition
]
->
PetriNet
makePetriNetWith
name
places
ts
initial
gs
=
let
transitions
=
map
fst
ts
buildMap
m
(
p
,
c
)
=
M
.
insertWith
addArc
p
c
m
addArc
(
lNew
,
rNew
)
(
lOld
,
rOld
)
=
(
lNew
++
lOld
,
rNew
++
rOld
)
placeArcs
=
[
(
i
,(
[]
,[(
t
,
w
)]))
|
(
t
,(
is
,
_
))
<-
ts
,
(
i
,
w
)
<-
is
]
++
[
(
o
,([(
t
,
w
)],
[]
))
|
(
t
,(
_
,
os
))
<-
ts
,
(
o
,
w
)
<-
os
]
placeMap
=
foldl
buildMap
M
.
empty
placeArcs
in
PetriNet
{
name
=
name
,
places
=
places
,
transitions
=
transitions
,
adjacencyP
=
placeMap
,
adjacencyT
=
M
.
fromList
ts
,
initialMarking
=
Marking
(
M
.
fromList
initial
),
ghostTransitions
=
gs
}
makePetriNetWithTrans
::
String
->
[
String
]
->
[(
String
,
[(
String
,
Integer
)],
[(
String
,
Integer
)])]
->
[(
String
,
Integer
)]
->
[
String
]
->
PetriNet
...
...
src/Printer/LOLA.hs
View file @
6456c0fb
...
...
@@ -32,8 +32,8 @@ renderNet net =
printNet
::
PetriNet
->
L
.
ByteString
printNet
=
toLazyByteString
.
renderNet
renderTerm
::
Term
->
Builder
renderTerm
(
Var
x
)
=
stringUtf8
x
renderTerm
::
(
Show
a
)
=>
Term
a
->
Builder
renderTerm
(
Var
x
)
=
stringUtf8
$
show
x
renderTerm
(
Const
c
)
=
integerDec
c
renderTerm
(
Minus
t
)
=
"-"
<>
renderTerm
t
renderTerm
(
t
:+:
u
)
=
"("
<>
renderTerm
t
<>
" + "
<>
renderTerm
u
<>
")"
...
...
@@ -48,15 +48,12 @@ renderOp Ne = " != "
renderOp
Le
=
" <= "
renderOp
Lt
=
" < "
renderLinIneq
::
LinearInequation
->
Builder
renderLinIneq
(
LinIneq
lhs
op
rhs
)
=
renderTerm
lhs
<>
renderOp
op
<>
renderTerm
rhs
-- TODO: reduce parantheses in built formula
renderFormula
::
Formula
->
Builder
renderFormula
::
(
Show
a
)
=>
Formula
a
->
Builder
renderFormula
FTrue
=
"TRUE"
renderFormula
FFalse
=
"FALSE"
renderFormula
(
Atom
a
)
=
renderLinIneq
a
renderFormula
(
LinearInequation
lhs
op
rhs
)
=
renderTerm
lhs
<>
renderOp
op
<>
renderTerm
rhs
renderFormula
(
Neg
p
)
=
"NOT "
<>
"("
<>
renderFormula
p
<>
")"
renderFormula
(
p
:&:
q
)
=
renderFormula
p
<>
" AND "
<>
renderFormula
q
renderFormula
(
p
:|:
q
)
=
"("
<>
renderFormula
p
<>
" OR "
<>
renderFormula
q
<>
")"
...
...
src/Printer/SARA.hs
View file @
6456c0fb
...
...
@@ -12,16 +12,16 @@ import Printer
import
PetriNet
import
Property
renderSimpleTerm
::
Integer
->
Term
->
Builder
renderSimpleTerm
fac
(
Var
x
)
=
if
fac
==
1
then
stringUtf8
x
else
integerDec
fac
<>
stringUtf8
x
renderSimpleTerm
::
Integer
->
Term
Place
->
Builder
renderSimpleTerm
fac
(
Var
x
)
=
if
fac
==
1
then
renderPlace
x
else
integerDec
fac
<>
renderPlace
x
renderSimpleTerm
fac
(
Const
c
)
=
integerDec
(
fac
*
c
)
renderSimpleTerm
fac
(
Const
c
:*:
t
)
=
renderSimpleTerm
(
fac
*
c
)
t
renderSimpleTerm
fac
(
t
:*:
Const
c
)
=
renderSimpleTerm
(
fac
*
c
)
t
renderSimpleTerm
fac
(
Minus
t
)
=
renderSimpleTerm
(
-
fac
)
t
renderSimpleTerm
_
t
=
error
$
"term not supported for sara: "
<>
show
t
renderTerm
::
Term
->
Builder
renderTerm
::
Term
Place
->
Builder
renderTerm
(
t
:+:
u
)
=
renderTerm
t
<>
"+"
<>
renderSimpleTerm
1
u
renderTerm
(
t
:-:
u
)
=
renderTerm
t
<>
"+"
<>
renderSimpleTerm
(
-
1
)
u
renderTerm
t
=
renderSimpleTerm
1
t
...
...
@@ -32,20 +32,19 @@ renderOp Eq = ":"
renderOp
Le
=
"<"
renderOp
op
=
error
$
"operand not supported for sara: "
<>
show
op
render
LinIneq
::
LinearInequation
->
Builder
render
LinIneq
(
LinIneq
lhs
op
(
Const
c
))
=
render
Conjunction
::
Formula
Place
->
Builder
render
Conjunction
(
Lin
ear
Ineq
uation
lhs
op
(
Const
c
))
=
renderTerm
lhs
<>
renderOp
op
<>
integerDec
c
renderLinIneq
l
=
error
$
"linear inequation not supported for sara: "
<>
show
l
renderConjunction
::
Formula
->
Builder
renderConjunction
(
Atom
a
)
=
renderLinIneq
a
renderConjunction
f
@
(
LinearInequation
{})
=
error
$
"linear inequation not supported for sara: "
<>
show
f
renderConjunction
(
Neg
_
)
=
error
"negation not supported for sara"
renderConjunction
(
FTrue
:&:
p
)
=
renderConjunction
p
renderConjunction
(
p
:&:
FTrue
)
=
renderConjunction
p
renderConjunction
(
p
:&:
q
)
=
renderConjunction
p
<>
", "
<>
renderConjunction
q
renderConjunction
f
=
error
$
"formula not supported for sara: "
<>
show
f
renderDisjunction
::
String
->
String
->
PetriNet
->
Formula
->
Builder
renderDisjunction
::
String
->
String
->
PetriNet
->
Formula
Place
->
Builder
renderDisjunction
propname
filename
net
(
FFalse
:|:
p
)
=
renderDisjunction
propname
filename
net
p
renderDisjunction
propname
filename
net
(
p
:|:
FFalse
)
=
...
...
@@ -64,7 +63,7 @@ renderDisjunction propname filename net f =
"FINAL COVER;
\n
"
<>
"CONSTRAINTS "
<>
renderConjunction
f
<>
";"
renderFormula
::
String
->
String
->
PetriNet
->
Formula
->
Builder
renderFormula
::
String
->
String
->
PetriNet
->
Formula
Place
->
Builder
renderFormula
=
renderDisjunction
renderProperty
::
String
->
PetriNet
->
Property
->
Builder
...
...
src/Printer/SPEC.hs
View file @
6456c0fb
...
...
@@ -14,26 +14,24 @@ renderOp :: Op -> Builder
renderOp
Ge
=
">="
renderOp
op
=
error
$
"operand not supported for spec: "
<>
show
op
renderLinIneq
::
LinearInequation
->
Builder
renderLinIneq
(
LinIneq
(
Var
x
)
op
(
Const
c
))
=
stringUtf8
x
<>
renderOp
op
<>
integerDec
c
renderLinIneq
l
=
error
$
"linear inequation not supported for spe: "
<>
show
l
renderConjunction
::
Formula
->
Builder
renderConjunction
(
Atom
a
)
=
renderLinIneq
a
renderConjunction
::
(
Show
a
)
=>
Formula
a
->
Builder
renderConjunction
(
LinearInequation
(
Var
x
)
op
(
Const
c
))
=
stringUtf8
(
show
x
)
<>
renderOp
op
<>
integerDec
c
renderConjunction
f
@
(
LinearInequation
{})
=
error
$
"linear inequation not supported for spec: "
<>
show
f
renderConjunction
(
Neg
_
)
=
error
"negation not supported for spec"
renderConjunction
(
FTrue
:&:
p
)
=
renderConjunction
p
renderConjunction
(
p
:&:
FTrue
)
=
renderConjunction
p
renderConjunction
(
p
:&:
q
)
=
renderConjunction
p
<>
", "
<>
renderConjunction
q
renderConjunction
f
=
error
$
"formula not supported for spec: "
<>
show
f
renderDisjunction
::
Formula
->
Builder
renderDisjunction
::
(
Show
a
)
=>
Formula
a
->
Builder
renderDisjunction
(
FFalse
:|:
p
)
=
renderDisjunction
p
renderDisjunction
(
p
:|:
FFalse
)
=
renderDisjunction
p
renderDisjunction
(
p
:|:
q
)
=
renderDisjunction
p
<>
"
\n
"
<>
renderDisjunction
q
renderDisjunction
f
=
renderConjunction
f
renderFormula
::
Formula
->
Builder
renderFormula
::
(
Show
a
)
=>
Formula
a
->
Builder
renderFormula
=
renderDisjunction
renderProperty
::
Property
->
Builder
...
...
src/Property.hs
View file @
6456c0fb
...
...
@@ -3,11 +3,10 @@
module
Property
(
Property
(
..
),
showPropertyName
,
rename
,
rename
Property
,
PropertyType
(
..
),
PropertyContent
(
..
),
Formula
(
..
),
LinearInequation
(
..
),
Op
(
..
),
Term
(
..
),
PropResult
(
..
),
...
...
@@ -18,31 +17,33 @@ module Property
resultsOr
)
where
import
PetriNet
import
Structure
data
Term
=
Var
String
|
Const
Integer
|
Minus
Term
|
Term
:+:
Term
|
Term
:-:
Term
|
Term
:*:
Term
deriving
(
Eq
)
instance
Show
Term
where
show
(
Var
x
)
=
x
data
Term
a
=
Var
a
|
Const
Integer
|
Minus
(
Term
a
)
|
Term
a
:+:
Term
a
|
Term
a
:-:
Term
a