Main.hs

module Main where

import System.Exit
import System.IO
import Control.Monad
import Control.Concurrent.ParallelIO
import Control.Arrow (first)
import Data.List (partition,minimumBy,genericLength)
import Data.Ord (comparing)
import Data.Maybe
import qualified Data.ByteString.Lazy as L
import Control.Monad.Reader

import Util
import Options
import Parser
import qualified Parser.PP as PPParser
import PopulationProtocol
import Printer
import qualified Printer.DOT as DOTPrinter
import Property
import StructuralComputation
import Solver
import Solver.LayeredTermination
import Solver.StrongConsensus

writeFiles :: String -> PopulationProtocol -> [Property] -> OptIO ()
writeFiles basename pp props = do
        format <- opt outputFormat
        verbosePut 1 $ "Writing " ++ showNetName pp ++ " to " ++
                                  basename ++ " in format " ++ show format
        case format of
            OutDOT ->
                liftIO $ L.writeFile basename $ DOTPrinter.printPopulationProtocol pp

structuralAnalysis :: PopulationProtocol -> OptIO ()
structuralAnalysis pp =  do
        verbosePut 0 $ "States             : " ++ show (length (states pp))
        verbosePut 0 $ "Transitions        : " ++ show (length (transitions pp))
        verbosePut 0 $ "Initial states     : " ++ show (length (initialStates pp))
        verbosePut 0 $ "Yes states         : " ++ show (length (trueStates pp))
        verbosePut 0 $ "No states          : " ++ show (length (falseStates pp))

checkFile :: String -> OptIO PropResult
checkFile file = do
        verbosePut 0 $ "Reading \"" ++ file ++ "\""
        format <- opt inputFormat
        let parser = case format of
                             InPP -> PPParser.parseContent
        pp <- liftIO $ parseFile parser file
        props <- opt optProperties
        verbosePut 1 $ "Analyzing " ++ showNetName pp
        verbosePut 2 $
                "Number of states: " ++ show (length (states pp))
        verbosePut 2 $
                "Number of transitions: " ++ show (length (transitions pp))
        let pRowSize p = let (preP, postP) = context pp p in length preP + length postP
        let arcs = sum $ map pRowSize $ states pp
        verbosePut 2 $
                "Number of arcs: " ++ show arcs
        printStruct <- opt optPrintStructure
        when printStruct $ structuralAnalysis pp
        verbosePut 3 $ show pp
        output <- opt optOutput
        case output of
            Just outputfile ->
                writeFiles outputfile pp props
            Nothing -> return ()
        -- TODO: short-circuit? parallel?
        rs <- mapM (checkProperty pp) props
        verbosePut 0 ""
        return $ resultsAnd rs


checkProperty :: PopulationProtocol -> Property -> OptIO PropResult
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) => [a] -> OptIO ()
printInvariant inv = do
        verbosePut 0 "Invariant found"
        let invSize = map invariantSize inv
        verbosePut 2 $ "Number of atoms in invariants: " ++ show invSize ++
                " (total of " ++ show (sum invSize) ++ ")"
        mapM_ (putLine . show) inv

checkStrongConsensus :: PopulationProtocol -> OptIO PropResult
checkStrongConsensus pp = do
        r <- checkStrongConsensus' pp ([], [])
        case r of
            (Nothing, _) -> return Satisfied
            (Just _, _) -> return Unknown

--checkStrongConsensus' :: PopulationProtocol -> RefinementObjects ->
--        OptIO (Maybe StrongConsensusCounterExample, RefinementObjects)
--checkStrongConsensus' pp refinements = do
--        optRefine <- opt optRefinementType
--        let method = case optRefine of
--                        RefAll -> checkStrongConsensusCompleteSat pp
--                        _ -> checkStrongConsensusSat pp refinements
--        r <- checkSat $ method
--        case r of
--            Nothing -> return (Nothing, refinements)
--            Just c -> do
--                case optRefine of
--                        RefDefault ->
--                            let refinementMethods = [TrapRefinement, SiphonRefinement, UTrapRefinement, USiphonRefinement]
--                            in refineStrongConsensus pp refinementMethods refinements c
--                        RefList refinementMethods ->
--                            refineStrongConsensus pp refinementMethods refinements c
--                        RefAll -> return (Nothing, refinements)

checkStrongConsensus' :: PopulationProtocol -> RefinementObjects ->
        OptIO (Maybe StrongConsensusCounterExample, RefinementObjects)
checkStrongConsensus' pp refinements = do
        optRefine <- opt optRefinementType
        case optRefine of
            RefAll -> do
                r <- checkSat $ checkStrongConsensusCompleteSat pp
                case r of
                    -- TODO unify counter example
                    Nothing -> return (Nothing, refinements)
                    Just (m0,m1,m2,x1,x2,_,_,_,_) -> return (Just (m0,m1,m2,x1,x2), refinements)
            _ -> do
                r <- checkSat $ checkStrongConsensusSat pp refinements
                case r of
                    Nothing -> return (Nothing, refinements)
                    Just c -> do
                        case optRefine of
                                RefDefault ->
                                    let refinementMethods = [TrapRefinement, SiphonRefinement, UTrapRefinement, USiphonRefinement]
                                    in refineStrongConsensus pp refinementMethods refinements c
                                RefList refinementMethods ->
                                    refineStrongConsensus pp refinementMethods refinements c
                                RefAll -> return (Nothing, refinements)

refineStrongConsensus :: PopulationProtocol -> [RefinementType] -> RefinementObjects ->
        StrongConsensusCounterExample ->
        OptIO (Maybe StrongConsensusCounterExample, RefinementObjects)
refineStrongConsensus pp [] refinements c = return (Just c, refinements)
refineStrongConsensus pp (ref:refs) refinements c = do
        let refinementMethod = case ref of
                         TrapRefinement -> Solver.StrongConsensus.findTrapConstraintsSat
                         SiphonRefinement -> Solver.StrongConsensus.findSiphonConstraintsSat
                         UTrapRefinement -> Solver.StrongConsensus.findUTrapConstraintsSat
                         USiphonRefinement -> Solver.StrongConsensus.findUSiphonConstraintsSat
        r <- checkSatMin $ refinementMethod pp c
        case r of
            Nothing -> do
                refineStrongConsensus pp refs refinements c
            Just refinement -> do
                let (utraps, usiphons) = refinements
                let refinements' = case ref of
                         TrapRefinement -> (refinement:utraps, usiphons)
                         SiphonRefinement -> (utraps, refinement:usiphons)
                         UTrapRefinement -> (refinement:utraps, usiphons)
                         USiphonRefinement -> (utraps, refinement:usiphons)
                checkStrongConsensus' pp refinements'

checkLayeredTermination :: PopulationProtocol -> OptIO PropResult
checkLayeredTermination pp = do
        let nonTrivialTriplets = filter (not . trivialTriplet) $ generateTriplets pp
        checkLayeredTermination' pp nonTrivialTriplets 1 $ genericLength $ transitions pp

checkLayeredTermination' :: PopulationProtocol -> [Triplet] -> Integer -> Integer -> OptIO PropResult
checkLayeredTermination' pp triplets k kmax = do
        verbosePut 1 $ "Checking layered termination with at most " ++ show k ++ " layers"
        r <- checkSatMin $ checkLayeredTerminationSat pp triplets k
        case r of
            Nothing ->
                if k < kmax then
                    checkLayeredTermination' pp triplets (k + 1) kmax
                else
                    return Unknown
            Just inv -> do
                invariant <- opt optInvariant
                when invariant $ printInvariant inv
                return Satisfied

main :: IO ()
main = do
        putStrLn "Peregrine - Efficient Verification of Population Protocols\n"
        args <- parseArgs
        case args of
            Left err -> exitErrorWith err
            Right (opts, files) -> do
                when (optShowVersion opts) (exitSuccessWith "Version 0.01")
                when (optShowHelp opts) (exitSuccessWith usageInformation)
                when (null files) (exitErrorWith "No input file given")
                rs <- runReaderT (mapM checkFile files) opts
                -- TODO: short-circuit with Control.Monad.Loops? parallel
                -- execution?
                let r = resultsAnd rs
                case r of
                    Satisfied ->
                        exitSuccessWith $ "All properties " ++ show r
                    _ ->
                        exitFailureWith $ "Some properties " ++ show r

exitSuccessWith :: String -> IO ()
exitSuccessWith msg = do
        putStrLn msg
        cleanupAndExitWith ExitSuccess

exitFailureWith :: String -> IO ()
exitFailureWith msg = do
        putStrLn msg
        cleanupAndExitWith $ ExitFailure 2

exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
        cleanupAndExitWith $ ExitFailure 3

cleanupAndExitWith :: ExitCode -> IO ()
cleanupAndExitWith code = do
        stopGlobalPool
        exitWith code