2.12.2021, 9:00 - 11:00: Due to updates GitLab may be unavailable for some minutes between 09:00 and 11:00.

Commit 4cdc7a42 authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Rename firing vector to flow vector

parent 6546c613
...@@ -2,16 +2,14 @@ ...@@ -2,16 +2,14 @@
{-# OPTIONS_GHC -fno-warn-name-shadowing #-} {-# OPTIONS_GHC -fno-warn-name-shadowing #-}
module PopulationProtocol module PopulationProtocol
(PopulationProtocol,State(..),Transition(..),Configuration,FiringVector, (PopulationProtocol,State(..),Transition(..),
RConfiguration,RFiringVector, Configuration,FlowVector,RConfiguration,RFlowVector,
renameState,renameTransition,renameStatesAndTransitions, renameState,renameTransition,renameStatesAndTransitions,
name,showNetName,states,transitions, name,showNetName,states,transitions,initialStates,yesStates,noStates,
initialStates,
pre,lpre,post,lpost,mpre,mpost,context, pre,lpre,post,lpost,mpre,mpost,context,
yesStates,noStates,
makePopulationProtocol,makePopulationProtocolWithTrans, makePopulationProtocol,makePopulationProtocolWithTrans,
makePopulationProtocolFromStrings,makePopulationProtocolWithTransFromStrings,Trap,Siphon, makePopulationProtocolFromStrings,makePopulationProtocolWithTransFromStrings,
Invariant(..)) Trap,Siphon,Invariant(..))
where where
import qualified Data.Map as M import qualified Data.Map as M
...@@ -58,10 +56,10 @@ instance Nodes Transition State where ...@@ -58,10 +56,10 @@ instance Nodes Transition State where
contextMap = adjacencyT contextMap = adjacencyT
type Configuration = IVector State type Configuration = IVector State
type FiringVector = IVector Transition type FlowVector = IVector Transition
type RConfiguration = RVector State type RConfiguration = RVector State
type RFiringVector = RVector Transition type RFlowVector = RVector Transition
type Trap = [State] type Trap = [State]
type Siphon = [State] type Siphon = [State]
......
...@@ -19,7 +19,7 @@ import PopulationProtocol ...@@ -19,7 +19,7 @@ import PopulationProtocol
import Property import Property
import Solver import Solver
type StrongConsensusCounterExample = (Configuration, Configuration, Configuration, FiringVector, FiringVector) type StrongConsensusCounterExample = (Configuration, Configuration, Configuration, FlowVector, FlowVector)
type StableInequality = (IMap State, Integer) type StableInequality = (IMap State, Integer)
...@@ -144,11 +144,11 @@ trapConstraints :: PopulationProtocol -> SIMap State -> SBool ...@@ -144,11 +144,11 @@ trapConstraints :: PopulationProtocol -> SIMap State -> SBool
trapConstraints pp b = trapConstraints pp b =
bAnd $ map (trapConstraint pp b) $ transitions pp bAnd $ map (trapConstraint pp b) $ transitions pp
uTrapConstraints :: PopulationProtocol -> FiringVector -> SIMap State -> SBool uTrapConstraints :: PopulationProtocol -> FlowVector -> SIMap State -> SBool
uTrapConstraints pp x b = uTrapConstraints pp x b =
bAnd $ map (trapConstraint pp b) $ elems x bAnd $ map (trapConstraint pp b) $ elems x
uSiphonConstraints :: PopulationProtocol -> FiringVector -> SIMap State -> SBool uSiphonConstraints :: PopulationProtocol -> FlowVector -> SIMap State -> SBool
uSiphonConstraints pp x b = uSiphonConstraints pp x b =
bAnd $ map (siphonConstraint pp b) $ elems x bAnd $ map (siphonConstraint pp b) $ elems x
...@@ -158,10 +158,10 @@ statesMarkedByConfiguration pp m b = sum (mval b $ elems m) .> 0 ...@@ -158,10 +158,10 @@ statesMarkedByConfiguration pp m b = sum (mval b $ elems m) .> 0
statesUnmarkedByConfiguration :: PopulationProtocol -> Configuration -> SIMap State -> SBool statesUnmarkedByConfiguration :: PopulationProtocol -> Configuration -> SIMap State -> SBool
statesUnmarkedByConfiguration pp m b = sum (mval b $ elems m) .== 0 statesUnmarkedByConfiguration pp m b = sum (mval b $ elems m) .== 0
statesPostsetOfSequence :: PopulationProtocol -> FiringVector -> SIMap State -> SBool statesPostsetOfSequence :: PopulationProtocol -> FlowVector -> SIMap State -> SBool
statesPostsetOfSequence pp x b = sum (mval b $ mpost pp $ elems x) .> 0 statesPostsetOfSequence pp x b = sum (mval b $ mpost pp $ elems x) .> 0
statesPresetOfSequence :: PopulationProtocol -> FiringVector -> SIMap State -> SBool statesPresetOfSequence :: PopulationProtocol -> FlowVector -> SIMap State -> SBool
statesPresetOfSequence pp x b = sum (mval b $ mpre pp $ elems x) .> 0 statesPresetOfSequence pp x b = sum (mval b $ mpre pp $ elems x) .> 0
noOutputTransitionEnabled :: PopulationProtocol -> Configuration -> SIMap State -> SBool noOutputTransitionEnabled :: PopulationProtocol -> Configuration -> SIMap State -> SBool
...@@ -189,7 +189,7 @@ minimizeMethod 1 curSize = "size smaller than " ++ show curSize ...@@ -189,7 +189,7 @@ minimizeMethod 1 curSize = "size smaller than " ++ show curSize
minimizeMethod 2 curSize = "size larger than " ++ show curSize minimizeMethod 2 curSize = "size larger than " ++ show curSize
minimizeMethod _ _ = error "minimization method not supported" minimizeMethod _ _ = error "minimization method not supported"
findTrap :: PopulationProtocol -> Configuration -> Configuration -> Configuration -> FiringVector -> FiringVector -> SIMap State -> Maybe (Int, Integer) -> SBool findTrap :: PopulationProtocol -> Configuration -> Configuration -> Configuration -> FlowVector -> FlowVector -> SIMap State -> Maybe (Int, Integer) -> SBool
findTrap pp m0 m1 m2 x1 x2 b sizeLimit = findTrap pp m0 m1 m2 x1 x2 b sizeLimit =
checkSizeLimit b sizeLimit &&& checkSizeLimit b sizeLimit &&&
checkBinary b &&& checkBinary b &&&
...@@ -199,7 +199,7 @@ findTrap pp m0 m1 m2 x1 x2 b sizeLimit = ...@@ -199,7 +199,7 @@ findTrap pp m0 m1 m2 x1 x2 b sizeLimit =
(statesPostsetOfSequence pp x2 b &&& statesUnmarkedByConfiguration pp m2 b) (statesPostsetOfSequence pp x2 b &&& statesUnmarkedByConfiguration pp m2 b)
) )
findTrapConstraintsSat :: PopulationProtocol -> Configuration -> Configuration -> Configuration -> FiringVector -> FiringVector -> MinConstraintProblem Integer Trap Integer findTrapConstraintsSat :: PopulationProtocol -> Configuration -> Configuration -> Configuration -> FlowVector -> FlowVector -> MinConstraintProblem Integer Trap Integer
findTrapConstraintsSat pp m0 m1 m2 x1 x2 = findTrapConstraintsSat pp m0 m1 m2 x1 x2 =
let b = makeVarMap $ states pp let b = makeVarMap $ states pp
in (minimizeMethod, \sizeLimit -> in (minimizeMethod, \sizeLimit ->
...@@ -208,7 +208,7 @@ findTrapConstraintsSat pp m0 m1 m2 x1 x2 = ...@@ -208,7 +208,7 @@ findTrapConstraintsSat pp m0 m1 m2 x1 x2 =
\fm -> findTrap pp m0 m1 m2 x1 x2 (fmap fm b) sizeLimit, \fm -> findTrap pp m0 m1 m2 x1 x2 (fmap fm b) sizeLimit,
\fm -> statesFromAssignment (fmap fm b))) \fm -> statesFromAssignment (fmap fm b)))
findUTrapConstraints :: PopulationProtocol -> Configuration -> Configuration -> Configuration -> FiringVector -> FiringVector -> SIMap State -> Maybe (Int, Integer) -> SBool findUTrapConstraints :: PopulationProtocol -> Configuration -> Configuration -> Configuration -> FlowVector -> FlowVector -> SIMap State -> Maybe (Int, Integer) -> SBool
findUTrapConstraints pp m0 m1 m2 x1 x2 b sizeLimit = findUTrapConstraints pp m0 m1 m2 x1 x2 b sizeLimit =
checkSizeLimit b sizeLimit &&& checkSizeLimit b sizeLimit &&&
checkBinary b &&& checkBinary b &&&
...@@ -217,7 +217,7 @@ findUTrapConstraints pp m0 m1 m2 x1 x2 b sizeLimit = ...@@ -217,7 +217,7 @@ findUTrapConstraints pp m0 m1 m2 x1 x2 b sizeLimit =
(statesPostsetOfSequence pp x2 b &&& uTrapConstraints pp x2 b &&& statesUnmarkedByConfiguration pp m2 b) (statesPostsetOfSequence pp x2 b &&& uTrapConstraints pp x2 b &&& statesUnmarkedByConfiguration pp m2 b)
) )
findUTrapConstraintsSat :: PopulationProtocol -> Configuration -> Configuration -> Configuration -> FiringVector -> FiringVector -> MinConstraintProblem Integer Trap Integer findUTrapConstraintsSat :: PopulationProtocol -> Configuration -> Configuration -> Configuration -> FlowVector -> FlowVector -> MinConstraintProblem Integer Trap Integer
findUTrapConstraintsSat pp m0 m1 m2 x1 x2 = findUTrapConstraintsSat pp m0 m1 m2 x1 x2 =
let b = makeVarMap $ states pp let b = makeVarMap $ states pp
in (minimizeMethod, \sizeLimit -> in (minimizeMethod, \sizeLimit ->
...@@ -226,7 +226,7 @@ findUTrapConstraintsSat pp m0 m1 m2 x1 x2 = ...@@ -226,7 +226,7 @@ findUTrapConstraintsSat pp m0 m1 m2 x1 x2 =
\fm -> findUTrapConstraints pp m0 m1 m2 x1 x2 (fmap fm b) sizeLimit, \fm -> findUTrapConstraints pp m0 m1 m2 x1 x2 (fmap fm b) sizeLimit,
\fm -> statesFromAssignment (fmap fm b))) \fm -> statesFromAssignment (fmap fm b)))
findUSiphonConstraints :: PopulationProtocol -> Configuration -> Configuration -> Configuration -> FiringVector -> FiringVector -> SIMap State -> Maybe (Int, Integer) -> SBool findUSiphonConstraints :: PopulationProtocol -> Configuration -> Configuration -> Configuration -> FlowVector -> FlowVector -> SIMap State -> Maybe (Int, Integer) -> SBool
findUSiphonConstraints pp m0 m1 m2 x1 x2 b sizeLimit = findUSiphonConstraints pp m0 m1 m2 x1 x2 b sizeLimit =
checkSizeLimit b sizeLimit &&& checkSizeLimit b sizeLimit &&&
checkBinary b &&& checkBinary b &&&
...@@ -236,7 +236,7 @@ findUSiphonConstraints pp m0 m1 m2 x1 x2 b sizeLimit = ...@@ -236,7 +236,7 @@ findUSiphonConstraints pp m0 m1 m2 x1 x2 b sizeLimit =
(statesPresetOfSequence pp x2 b &&& uSiphonConstraints pp x2 b) (statesPresetOfSequence pp x2 b &&& uSiphonConstraints pp x2 b)
) )
findUSiphonConstraintsSat :: PopulationProtocol -> Configuration -> Configuration -> Configuration -> FiringVector -> FiringVector -> MinConstraintProblem Integer Siphon Integer findUSiphonConstraintsSat :: PopulationProtocol -> Configuration -> Configuration -> Configuration -> FlowVector -> FlowVector -> MinConstraintProblem Integer Siphon Integer
findUSiphonConstraintsSat pp m0 m1 m2 x1 x2 = findUSiphonConstraintsSat pp m0 m1 m2 x1 x2 =
let b = makeVarMap $ states pp let b = makeVarMap $ states pp
in (minimizeMethod, \sizeLimit -> in (minimizeMethod, \sizeLimit ->
...@@ -275,14 +275,14 @@ checkGeneralizedCoTrap :: PopulationProtocol -> SIMap State -> SInteger -> SBool ...@@ -275,14 +275,14 @@ checkGeneralizedCoTrap :: PopulationProtocol -> SIMap State -> SInteger -> SBool
checkGeneralizedCoTrap pp k c = checkGeneralizedCoTrap pp k c =
bAnd [ checkGeneralizedTCoTrap pp k c t | t <- transitions pp ] bAnd [ checkGeneralizedTCoTrap pp k c t | t <- transitions pp ]
checkGeneralizedCoTrapConstraints :: PopulationProtocol -> Configuration -> Configuration -> Configuration -> FiringVector -> FiringVector -> SIMap State -> SInteger -> SBool checkGeneralizedCoTrapConstraints :: PopulationProtocol -> Configuration -> Configuration -> Configuration -> FlowVector -> FlowVector -> SIMap State -> SInteger -> SBool
checkGeneralizedCoTrapConstraints pp m0 m1 m2 x1 x2 k c = checkGeneralizedCoTrapConstraints pp m0 m1 m2 x1 x2 k c =
checkSemiNegativeConstraints k &&& checkSemiNegativeConstraints k &&&
checkGeneralizedCoTrap pp k c &&& checkGeneralizedCoTrap pp k c &&&
checkStableInequalityForConfiguration pp m0 k c &&& checkStableInequalityForConfiguration pp m0 k c &&&
((bnot (checkStableInequalityForConfiguration pp m1 k c)) ||| (bnot (checkStableInequalityForConfiguration pp m2 k c))) ((bnot (checkStableInequalityForConfiguration pp m1 k c)) ||| (bnot (checkStableInequalityForConfiguration pp m2 k c)))
checkGeneralizedCoTrapSat :: PopulationProtocol -> Configuration -> Configuration -> Configuration -> FiringVector -> FiringVector -> ConstraintProblem Integer StableInequality checkGeneralizedCoTrapSat :: PopulationProtocol -> Configuration -> Configuration -> Configuration -> FlowVector -> FlowVector -> ConstraintProblem Integer StableInequality
checkGeneralizedCoTrapSat pp m0 m1 m2 x1 x2 = checkGeneralizedCoTrapSat pp m0 m1 m2 x1 x2 =
let k = makeVarMap $ states pp let k = makeVarMap $ states pp
c = "'c" c = "'c"
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment