Rename options and properties

src/Main.hs

@@ -21,8 +21,8 @@ import qualified Printer.DOT as DOTPrinter
 import Property
 import StructuralComputation
 import Solver
-import Solver.TerminalMarkingsUniqueConsensus
-import Solver.TerminalMarkingReachable
+import Solver.LayeredTermination
+import Solver.StrongConsensus
 
 writeFiles :: String -> PopulationProtocol -> [Property] -> OptIO ()
 writeFiles basename pp props = do
@@ -47,9 +47,8 @@ checkFile file = do
         format <- opt inputFormat
         let parser = case format of
                              InPP -> PPParser.parseContent
-        (pp,props) <- liftIO $ parseFile parser file
-        implicitProperties <- opt optProperties
-        let props' = props ++ map (makeImplicitProperty pp) implicitProperties
+        pp <- liftIO $ parseFile parser file
+        props <- opt optProperties
         verbosePut 1 $ "Analyzing " ++ showNetName pp
         verbosePut 2 $
                 "Number of states: " ++ show (length (states pp))
@@ -65,33 +64,22 @@ checkFile file = do
         output <- opt optOutput
         case output of
             Just outputfile ->
-                writeFiles outputfile pp props'
+                writeFiles outputfile pp props
             Nothing -> return ()
         -- TODO: short-circuit? parallel?
-        rs <- mapM (checkProperty pp) props'
+        rs <- mapM (checkProperty pp) props
         verbosePut 0 ""
         return $ resultsAnd rs
 
 
-makeImplicitProperty :: PopulationProtocol -> ImplicitProperty -> Property
-makeImplicitProperty _ TerminalMarkingsUniqueConsensus =
-        Property "reachable terminal markings have a unique consensus" $ Constraint TerminalMarkingsUniqueConsensusConstraint
-makeImplicitProperty _ TerminalMarkingReachable =
-        Property "terminal marking reachable" $ Constraint TerminalMarkingReachableConstraint
-
 checkProperty :: PopulationProtocol -> Property -> OptIO PropResult
-checkProperty pp p = do
-        verbosePut 1 $ "\nChecking " ++ showPropertyName p
-        verbosePut 3 $ show p
-        r <- case pcont p of
---            (Safety pf) -> checkSafetyProperty pp pf
---            (Liveness pf) -> checkLivenessProperty pp pf
-            (Constraint pc) -> checkConstraintProperty pp pc
-        verbosePut 0 $ showPropertyName p ++ " " ++
-            case r of
-                Satisfied -> "is satisfied."
-                Unsatisfied -> "is not satisfied."
-                Unknown-> "may not be satisfied."
+checkProperty pp prop = do
+        verbosePut 1 $ "\nChecking " ++ show prop
+        r <- case prop of
+                Correctness -> error "not yet implemented"
+                LayeredTermination -> checkLayeredTermination pp
+                StrongConsensus -> checkStrongConsensus pp
+        verbosePut 0 $ show prop ++ " " ++ show r
         return r
 
 printInvariant :: (Show a, Invariant a) => (Maybe [a], [a]) -> OptIO PropResult
@@ -112,66 +100,60 @@ printInvariant (baseInvResult, addedInv) =
                 mapM_ (putLine . show) addedInv
                 return Satisfied
 
-checkConstraintProperty :: PopulationProtocol -> ConstraintProperty -> OptIO PropResult
-checkConstraintProperty pp cp =
-        case cp of
-            TerminalMarkingsUniqueConsensusConstraint -> checkTerminalMarkingsUniqueConsensusProperty pp
-            TerminalMarkingReachableConstraint -> checkTerminalMarkingReachableProperty pp
-
-checkTerminalMarkingsUniqueConsensusProperty :: PopulationProtocol -> OptIO PropResult
-checkTerminalMarkingsUniqueConsensusProperty pp = do
-        r <- checkTerminalMarkingsUniqueConsensusProperty' pp [] [] []
+checkStrongConsensus :: PopulationProtocol -> OptIO PropResult
+checkStrongConsensus pp = do
+        r <- checkStrongConsensus' pp [] [] []
         case r of
             (Nothing, _, _, _) -> return Satisfied
             (Just _, _, _, _) -> return Unknown
 
-checkTerminalMarkingsUniqueConsensusProperty' :: PopulationProtocol ->
+checkStrongConsensus' :: PopulationProtocol ->
         [Trap] -> [Siphon] -> [StableInequality] ->
-        OptIO (Maybe TerminalMarkingsUniqueConsensusCounterExample, [Trap], [Siphon], [StableInequality])
-checkTerminalMarkingsUniqueConsensusProperty' pp utraps usiphons inequalities = do
-        r <- checkSat $ checkTerminalMarkingsUniqueConsensusSat pp utraps usiphons inequalities
+        OptIO (Maybe StrongConsensusCounterExample, [Trap], [Siphon], [StableInequality])
+checkStrongConsensus' pp utraps usiphons inequalities = do
+        r <- checkSat $ checkStrongConsensusSat pp utraps usiphons inequalities
         case r of
             Nothing -> return (Nothing, utraps, usiphons, inequalities)
             Just c -> do
                 refine <- opt optRefinementType
                 if isJust refine then
-                    refineTerminalMarkingsUniqueConsensusProperty pp utraps usiphons inequalities c
+                    refineStrongConsensus pp utraps usiphons inequalities c
                 else
                     return (Just c, utraps, usiphons, inequalities)
 
-refineTerminalMarkingsUniqueConsensusProperty :: PopulationProtocol ->
-        [Trap] -> [Siphon] -> [StableInequality] -> TerminalMarkingsUniqueConsensusCounterExample ->
-        OptIO (Maybe TerminalMarkingsUniqueConsensusCounterExample, [Trap], [Siphon], [StableInequality])
-refineTerminalMarkingsUniqueConsensusProperty pp utraps usiphons inequalities c@(m0, m1, m2, x1, x2) = do
-        r1 <- checkSatMin $ Solver.TerminalMarkingsUniqueConsensus.findTrapConstraintsSat pp m0 m1 m2 x1 x2
+refineStrongConsensus :: PopulationProtocol ->
+        [Trap] -> [Siphon] -> [StableInequality] -> StrongConsensusCounterExample ->
+        OptIO (Maybe StrongConsensusCounterExample, [Trap], [Siphon], [StableInequality])
+refineStrongConsensus pp utraps usiphons inequalities c@(m0, m1, m2, x1, x2) = do
+        r1 <- checkSatMin $ Solver.StrongConsensus.findTrapConstraintsSat pp m0 m1 m2 x1 x2
         case r1 of
             Nothing -> do
-                r2 <- checkSatMin $ Solver.TerminalMarkingsUniqueConsensus.findUSiphonConstraintsSat pp m0 m1 m2 x1 x2
+                r2 <- checkSatMin $ Solver.StrongConsensus.findUSiphonConstraintsSat pp m0 m1 m2 x1 x2
                 case r2 of
                     Nothing -> do
-                        r3 <- checkSatMin $ Solver.TerminalMarkingsUniqueConsensus.findUTrapConstraintsSat pp m0 m1 m2 x1 x2
+                        r3 <- checkSatMin $ Solver.StrongConsensus.findUTrapConstraintsSat pp m0 m1 m2 x1 x2
                         case r3 of
                             Nothing -> return (Just c, utraps, usiphons, inequalities)
                             Just utrap ->
-                                checkTerminalMarkingsUniqueConsensusProperty' pp (utrap:utraps) usiphons inequalities
+                                checkStrongConsensus' pp (utrap:utraps) usiphons inequalities
                     Just usiphon ->
-                        checkTerminalMarkingsUniqueConsensusProperty' pp utraps (usiphon:usiphons) inequalities
+                        checkStrongConsensus' pp utraps (usiphon:usiphons) inequalities
             Just trap ->
-                checkTerminalMarkingsUniqueConsensusProperty' pp (trap:utraps) usiphons inequalities
+                checkStrongConsensus' pp (trap:utraps) usiphons inequalities
 
-checkTerminalMarkingReachableProperty :: PopulationProtocol -> OptIO PropResult
-checkTerminalMarkingReachableProperty pp = do
+checkLayeredTermination :: PopulationProtocol -> OptIO PropResult
+checkLayeredTermination pp = do
         let nonTrivialTriplets = filter (not . trivialTriplet) $ generateTriplets pp
-        checkTerminalMarkingReachableProperty' pp nonTrivialTriplets 1 $ genericLength $ transitions pp
+        checkLayeredTermination' pp nonTrivialTriplets 1 $ genericLength $ transitions pp
 
-checkTerminalMarkingReachableProperty' :: PopulationProtocol -> [Triplet] -> Integer -> Integer -> OptIO PropResult
-checkTerminalMarkingReachableProperty' pp triplets k kmax = do
+checkLayeredTermination' :: PopulationProtocol -> [Triplet] -> Integer -> Integer -> OptIO PropResult
+checkLayeredTermination' pp triplets k kmax = do
         verbosePut 1 $ "Checking terminal marking reachable with at most " ++ show k ++ " partitions"
-        r <- checkSatMin $ checkTerminalMarkingReachableSat pp triplets k
+        r <- checkSatMin $ checkLayeredTerminationSat pp triplets k
         case r of
             Nothing ->
                 if k < kmax then
-                    checkTerminalMarkingReachableProperty' pp triplets (k + 1) kmax
+                    checkLayeredTermination' pp triplets (k + 1) kmax
                 else
                     return Unknown
             Just inv -> do
@@ -195,15 +177,13 @@ main = do
                 rs <- runReaderT (mapM checkFile files) opts'
                 -- TODO: short-circuit with Control.Monad.Loops? parallel
                 -- execution?
-                case resultsAnd rs of
+                let r = resultsAnd rs
+                case r of
                     Satisfied ->
-                        exitSuccessWith "All properties satisfied."
-                    Unsatisfied ->
-                        exitFailureWith "Some properties are not satisfied"
-                    Unknown ->
-                        exitFailureWith "Some properties may not be satisfied."
+                        exitSuccessWith $ "All properties " ++ show r
+                    _ ->
+                        exitFailureWith $ "Some properties " ++ show r
 
--- TODO: Always exit with exit code 0 unless an error occured
 exitSuccessWith :: String -> IO ()
 exitSuccessWith msg = do
         putStrLn msg

src/Options.hs

@@ -2,7 +2,7 @@
 
 module Options
     (InputFormat(..),OutputFormat(..),RefinementType(..),
-     ImplicitProperty(..),Options(..),startOptions,options,parseArgs,
+     Options(..),startOptions,options,parseArgs,
      usageInformation)
 where
 
@@ -10,6 +10,8 @@ import Control.Applicative ((<$>))
 import System.Console.GetOpt
 import System.Environment (getArgs)
 
+import Property (Property(..))
+
 data InputFormat = InPP deriving (Read)
 data OutputFormat = OutDOT deriving (Read)
 
@@ -18,10 +20,6 @@ instance Show InputFormat where
 instance Show OutputFormat where
         show OutDOT = "DOT"
 
-data ImplicitProperty = TerminalMarkingsUniqueConsensus
-                      | TerminalMarkingReachable
-                      deriving (Show,Read)
-
 data RefinementType = TrapRefinement
                     | SiphonRefinement
                     | UTrapRefinement
@@ -32,12 +30,11 @@ data Options = Options { inputFormat :: InputFormat
                        , optVerbosity :: Int
                        , optShowHelp :: Bool
                        , optShowVersion :: Bool
-                       , optProperties :: [ImplicitProperty]
+                       , optProperties :: [Property]
                        , optRefinementType :: Maybe [RefinementType]
                        , optMinimizeRefinement :: Int
                        , optSMTAuto :: Bool
                        , optInvariant :: Bool
-                       , optBoolConst :: Bool
                        , optOutput :: Maybe String
                        , outputFormat :: OutputFormat
                        , optUseProperties :: Bool
@@ -54,7 +51,6 @@ startOptions = Options { inputFormat = InPP
                        , optMinimizeRefinement = 0
                        , optSMTAuto = True
                        , optInvariant = False
-                       , optBoolConst = False
                        , optOutput = Nothing
                        , outputFormat = OutDOT
                        , optUseProperties = True
@@ -63,35 +59,22 @@ startOptions = Options { inputFormat = InPP
 
 options :: [ OptDescr (Options -> Either String Options) ]
 options =
-        [ Option "" ["pp"]
-        (NoArg (\opt -> Right opt { inputFormat = InPP }))
-        "Use the population protocol input format"
-
-        , Option "" ["structure"]
-        (NoArg (\opt -> Right opt { optPrintStructure = True }))
-        "Print structural information"
-
-        , Option "" ["terminal-markings-unique-consensus"]
+        [ Option "" ["layered-termination"]
         (NoArg (\opt -> Right opt {
-                   optProperties = optProperties opt ++ [TerminalMarkingsUniqueConsensus]
+                   optProperties = optProperties opt ++ [LayeredTermination]
                }))
-        "Prove that terminal markings have a unique consensus"
+        "Prove that the protocol satisfies layered termination"
 
-        , Option "" ["terminal-marking-reachable"]
+        , Option "" ["strong-consensus"]
         (NoArg (\opt -> Right opt {
-                   optProperties = optProperties opt ++ [TerminalMarkingReachable]
+                   optProperties = optProperties opt ++ [StrongConsensus]
                }))
-        "Prove that a terminal marking is reachable"
+        "Prove that the protocol satisfies strong consensus"
 
         , Option "i" ["invariant"]
         (NoArg (\opt -> Right opt { optInvariant = True }))
         "Generate an invariant"
 
-        , Option "" ["bool-const"]
-        (NoArg (\opt -> Right opt { optBoolConst = True }))
-        ("Use boolean constraints instead of integer ones\n" ++
-         "  for transition invariant")
-
         , Option "r" ["refinement"]
         (ReqArg (\arg opt ->
                     let addRef ref =
@@ -111,6 +94,16 @@ options =
                 "METHOD")
         ("Refine with METHOD (trap, siphon, utrap, usiphon)")
 
+        , Option "s" ["structure"]
+        (NoArg (\opt -> Right opt { optPrintStructure = True }))
+        "Print structural information"
+
+
+        , Option "" ["in-pp"]
+        (NoArg (\opt -> Right opt { inputFormat = InPP }))
+        "Use the population protocol input format"
+
+
         , Option "o" ["output"]
         (ReqArg (\arg opt -> Right opt {
                         optOutput = Just arg

src/Parser/PP.hs

@@ -187,29 +187,17 @@ formAtom =  try linIneq
 formula :: Parser (Formula String)
 formula = buildExpressionParser formOperatorTable formAtom <?> "formula"
 
-propertyType :: Parser PropertyType
-propertyType =
-        (reserved "safety" *> return SafetyType) <|>
-        (reserved "liveness" *> return LivenessType)
-
-property :: Parser Property
-property = do
-        pt <- propertyType
-        reserved "property"
+predicate :: Parser (Formula PopulationProtocol.State)
+predicate = do
+        reserved "predicate"
         name <- option "" ident
-        case pt of
-            SafetyType -> do
-                form <- braces formula
-                return Property
-                    { pname=name, pcont=Safety (fmap PopulationProtocol.State form) }
-            LivenessType -> do
-                form <- braces formula
-                return Property { pname=name, pcont=Liveness (fmap Transition form) }
-
-parseContent :: Parser (PopulationProtocol,[Property])
+        form <- braces formula
+        return (fmap PopulationProtocol.State form)
+
+parseContent :: Parser PopulationProtocol
 parseContent = do
         whiteSpace
         pp <- populationProtocol
-        properties <- many property
+--        properties <- many predicate
         eof
-        return (pp, properties)
+        return pp

src/Property.hs

@@ -2,11 +2,6 @@
 
 module Property
     (Property(..),
-     showPropertyName,
-     renameProperty,
-     PropertyType(..),
-     PropertyContent(..),
-     ConstraintProperty(..),
      Formula(..),
      Op(..),
      Term(..),
@@ -18,8 +13,6 @@ module Property
      resultsOr)
 where
 
-import PopulationProtocol
-
 data Term a =
           Var a
         | Const Integer
@@ -84,58 +77,21 @@ instance Functor Formula where
         fmap f (p :&: q) = fmap f p :&: fmap f q
         fmap f (p :|: q) = fmap f p :|: fmap f q
 
--- TODO: add functions to transform formula to CNF/DNF
-
-data PropertyType = SafetyType
-                  | LivenessType
-                  | ConstraintType
-
-data ConstraintProperty = TerminalMarkingsUniqueConsensusConstraint
-                        | TerminalMarkingReachableConstraint
-
-instance Show ConstraintProperty where
-        show TerminalMarkingsUniqueConsensusConstraint = "reachable terminal markings have a unique consensus"
-        show TerminalMarkingReachableConstraint = "terminal marking reachable"
-
-data PropertyContent = Safety (Formula State)
-                  | Liveness (Formula Transition)
-                  | Constraint ConstraintProperty
+data Property = Correctness
+              | LayeredTermination
+              | StrongConsensus
 
-showPropertyType :: PropertyContent -> String
-showPropertyType (Safety _) = "safety"
-showPropertyType (Liveness _) = "liveness"
-showPropertyType (Constraint _) = "constraint"
-
-showPropertyContent :: PropertyContent -> String
-showPropertyContent (Safety f) = show f
-showPropertyContent (Liveness f) = show f
-showPropertyContent (Constraint c) = show c
-
-instance Show PropertyContent where
-        show pc = showPropertyType pc ++ " (" ++ showPropertyContent pc ++ ")"
+instance Show Property where
+        show Correctness = "correctness"
+        show LayeredTermination = "layered termination"
+        show StrongConsensus = "strong consensus"
 
-data Property = Property {
-        pname :: String,
-        pcont :: PropertyContent
-}
+data PropResult = Satisfied | Unsatisfied | Unknown deriving (Eq)
 
-instance Show Property where
-        show p =
-            showPropertyName p ++
-            " { " ++ showPropertyContent (pcont p) ++ " }"
-
-renameProperty :: (String -> String) -> Property -> Property
-renameProperty f (Property pn (Safety pf)) =
-        Property pn (Safety (fmap (renameState f) pf))
-renameProperty f (Property pn (Liveness pf)) =
-        Property pn (Liveness (fmap (renameTransition f) pf))
-renameProperty _ p = p
-
-showPropertyName :: Property -> String
-showPropertyName p = showPropertyType (pcont p) ++ " property" ++
-               (if null (pname p) then "" else " " ++ show (pname p))
-
-data PropResult = Satisfied | Unsatisfied | Unknown deriving (Show,Read,Eq)
+instance Show PropResult where
+        show Satisfied = "satisfied"
+        show Unsatisfied = "not satisfied"
+        show Unknown = "may not be satisfied"
 
 resultAnd :: PropResult -> PropResult -> PropResult
 resultAnd Satisfied x = x

src/Solver/TerminalMarkingReachable.hs → src/Solver/LayeredTermination.hs

 {-# LANGUAGE FlexibleContexts #-}
 
-module Solver.TerminalMarkingReachable
-    (checkTerminalMarkingReachableSat,
-     TerminalMarkingReachableInvariant)
+module Solver.LayeredTermination
+    (checkLayeredTerminationSat,
+     LayeredTerminationInvariant)
 where
 
 import Data.SBV
@@ -17,15 +17,15 @@ import StructuralComputation
 
 type InvariantSize = ([Int], [Integer], [Int])
 
-type TerminalMarkingReachableInvariant = [BlockInvariant]
-data BlockInvariant =
-            BlockInvariant (Integer, [Transition], IVector State)
+type LayeredTerminationInvariant = [LayerInvariant]
+data LayerInvariant =
+            LayerInvariant (Integer, [Transition], IVector State)
 
-instance Invariant BlockInvariant where
-        invariantSize (BlockInvariant (_, ti, yi)) = if null ti then 0 else size yi
+instance Invariant LayerInvariant where
+        invariantSize (LayerInvariant (_, ti, yi)) = if null ti then 0 else size yi
 
-instance Show BlockInvariant where
-        show (BlockInvariant (i, ti, yi)) =
+instance Show LayerInvariant where
+        show (LayerInvariant (i, ti, yi)) =
                 "T_" ++ show i ++ ":\n" ++ unlines (map show ti) ++
                     (if null ti then "" else "\nY_" ++ show i ++ ": " ++ intercalate " + " (map showWeighted (items yi)) ++ "\n")
 
@@ -38,8 +38,8 @@ checkNonNegativityConstraints :: (Ord a, Show a) => [SIMap a] -> SBool
 checkNonNegativityConstraints xs =
             bAnd $ map nonNegativityConstraints xs
 
-blockTerminationConstraints :: PopulationProtocol -> Integer -> SIMap Transition -> SIMap State -> SBool
-blockTerminationConstraints pp i b y =
+layerTerminationConstraints :: PopulationProtocol -> Integer -> SIMap Transition -> SIMap State -> SBool
+layerTerminationConstraints pp i b y =
             bAnd $ map checkTransition $ transitions pp
         where checkTransition t =
                 let incoming = map addState $ lpre pp t
@@ -49,46 +49,46 @@ blockTerminationConstraints pp i b y =
 
 terminationConstraints :: PopulationProtocol -> Integer -> SIMap Transition -> [SIMap State] -> SBool
 terminationConstraints pp k b ys =
-        bAnd $ [blockTerminationConstraints pp i b y | (i,y) <- zip [1..] ys]
+        bAnd $ [layerTerminationConstraints pp i b y | (i,y) <- zip [1..] ys]
 
-blockConstraints :: PopulationProtocol -> Integer -> SIMap Transition -> SBool
-blockConstraints pp k b =
-            bAnd $ map checkBlock $ transitions pp
-        where checkBlock t = literal 1 .<= val b t &&& val b t .<= literal k
+layerConstraints :: PopulationProtocol -> Integer -> SIMap Transition -> SBool
+layerConstraints pp k b =
+            bAnd $ map checkLayer $ transitions pp
+        where checkLayer t = literal 1 .<= val b t &&& val b t .<= literal k
 
-blockOrderConstraints :: PopulationProtocol -> [Triplet] -> Integer -> SIMap Transition -> SBool
-blockOrderConstraints pp triplets k b =
+layerOrderConstraints :: PopulationProtocol -> [Triplet] -> Integer -> SIMap Transition -> SBool
+layerOrderConstraints pp triplets k b =
             bAnd $ map checkTriplet triplets
         where checkTriplet (s,t,ts) = (val b s .> val b t) ==> bOr (map (\t' -> val b t' .== val b t) ts)
 
-checkTerminalMarkingReachable :: PopulationProtocol -> [Triplet] -> Integer -> SIMap Transition -> [SIMap State] -> Maybe (Int, InvariantSize) -> SBool
-checkTerminalMarkingReachable pp triplets k b ys sizeLimit =
-        blockConstraints pp k b &&&
+checkLayeredTermination :: PopulationProtocol -> [Triplet] -> Integer -> SIMap Transition -> [SIMap State] -> Maybe (Int, InvariantSize) -> SBool
+checkLayeredTermination pp triplets k b ys sizeLimit =
+        layerConstraints pp k b &&&
         terminationConstraints pp k b ys &&&
-        blockOrderConstraints pp triplets k b &&&
+        layerOrderConstraints pp triplets k b &&&
         checkNonNegativityConstraints ys &&&
         checkSizeLimit k b ys sizeLimit
 
-checkTerminalMarkingReachableSat :: PopulationProtocol -> [Triplet] -> Integer -> MinConstraintProblem Integer TerminalMarkingReachableInvariant InvariantSize
-checkTerminalMarkingReachableSat pp triplets k =
+checkLayeredTerminationSat :: PopulationProtocol -> [Triplet] -> Integer -> MinConstraintProblem Integer LayeredTerminationInvariant InvariantSize
+checkLayeredTerminationSat pp triplets k =
         let makeYName i = (++) (genericReplicate i '\'')
             ys = [makeVarMapWith (makeYName i) $ states pp | i <- [1..k]]
             b = makeVarMap $ transitions pp