diff --git a/Control/Concurrent/CHPSpec.hs b/Control/Concurrent/CHPSpec.hs new file mode 100644 --- /dev/null +++ b/Control/Concurrent/CHPSpec.hs @@ -0,0 +1,55 @@ +-- Communicating Haskell Processes. +-- Copyright (c) 2008, University of Kent. +-- All rights reserved. +-- +-- Redistribution and use in source and binary forms, with or without +-- modification, are permitted provided that the following conditions are +-- met: +-- +-- * Redistributions of source code must retain the above copyright +-- notice, this list of conditions and the following disclaimer. +-- * Redistributions in binary form must reproduce the above copyright +-- notice, this list of conditions and the following disclaimer in the +-- documentation and/or other materials provided with the distribution. +-- * Neither the name of the University of Kent nor the names of its +-- contributors may be used to endorse or promote products derived from +-- this software without specific prior written permission. +-- +-- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +-- IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, +-- THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +-- PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +-- CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +-- EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +-- PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +-- PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +-- LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +-- NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +-- SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + +-- | This module re-exports all of the functionality of the chp-spec library, except +-- the "Control.Concurrent.CHPSpec.LazySmallCheck" module. +-- +-- The documentation for this library may seem relatively spartan; only the functions +-- and modules with significant differences\/caveats from CHP API are documented. +-- All the details of how each aspect is modelled is available in the original +-- series of blog posts. +module Control.Concurrent.CHPSpec ( + module Control.Concurrent.CHPSpec.Alt, + module Control.Concurrent.CHPSpec.Barriers, + module Control.Concurrent.CHPSpec.Channels, + module Control.Concurrent.CHPSpec.Enroll, + module Control.Concurrent.CHPSpec.Monad, + module Control.Concurrent.CHPSpec.Parallel + ) where + +import Control.Concurrent.CHPSpec.Alt +import Control.Concurrent.CHPSpec.Barriers +import Control.Concurrent.CHPSpec.Channels +import Control.Concurrent.CHPSpec.Enroll +import Control.Concurrent.CHPSpec.Monad +import Control.Concurrent.CHPSpec.Parallel + + + + diff --git a/Control/Concurrent/CHPSpec/Alt.hs b/Control/Concurrent/CHPSpec/Alt.hs new file mode 100644 --- /dev/null +++ b/Control/Concurrent/CHPSpec/Alt.hs @@ -0,0 +1,57 @@ +-- Communicating Haskell Processes. +-- Copyright (c) 2008-2010, University of Kent, Neil Brown. +-- All rights reserved. +-- +-- Redistribution and use in source and binary forms, with or without +-- modification, are permitted provided that the following conditions are +-- met: +-- +-- * Redistributions of source code must retain the above copyright +-- notice, this list of conditions and the following disclaimer. +-- * Redistributions in binary form must reproduce the above copyright +-- notice, this list of conditions and the following disclaimer in the +-- documentation and/or other materials provided with the distribution. +-- * Neither the name of the University of Kent nor the names of its +-- contributors may be used to endorse or promote products derived from +-- this software without specific prior written permission. +-- +-- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +-- IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, +-- THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +-- PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +-- CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +-- EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +-- PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +-- PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +-- LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +-- NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +-- SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + + +-- | A module containing the choice constructs. See +-- for details of how choice is modelled. +-- +-- Currently conjunction is not modelled (mainly because CSP\/FDR don't support +-- it), but external choice is modelled fine; 'priAlt' is modelled as a plain 'alt', +-- though. +module Control.Concurrent.CHPSpec.Alt (alt, (<->), priAlt, ()) where + +import Control.Concurrent.CHPSpec.Base +import Control.Concurrent.CHPSpec.Spec + +alt :: [CHP a] -> CHP a +alt = priAlt + +priAlt :: [CHP a] -> CHP a +priAlt [] = stopSpecT $ return Stop +priAlt ps = altSpecT ps + +(<->) :: CHP a -> CHP a -> CHP a +(<->) a b = alt [a,b] + +() :: CHP a -> CHP a -> CHP a +() a b = priAlt [a,b] + +infixl +infixl <-> + diff --git a/Control/Concurrent/CHPSpec/Barriers.hs b/Control/Concurrent/CHPSpec/Barriers.hs new file mode 100644 --- /dev/null +++ b/Control/Concurrent/CHPSpec/Barriers.hs @@ -0,0 +1,84 @@ +-- Communicating Haskell Processes. +-- Copyright (c) 2008-2010, University of Kent, Neil Brown. +-- All rights reserved. +-- +-- Redistribution and use in source and binary forms, with or without +-- modification, are permitted provided that the following conditions are +-- met: +-- +-- * Redistributions of source code must retain the above copyright +-- notice, this list of conditions and the following disclaimer. +-- * Redistributions in binary form must reproduce the above copyright +-- notice, this list of conditions and the following disclaimer in the +-- documentation and/or other materials provided with the distribution. +-- * Neither the name of the University of Kent nor the names of its +-- contributors may be used to endorse or promote products derived from +-- this software without specific prior written permission. +-- +-- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +-- IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, +-- THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +-- PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +-- CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +-- EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +-- PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +-- PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +-- LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +-- NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +-- SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + +-- | A module containing barriers. +-- +-- The 'PhasedBarrier' type remains, but currently 'syncBarrier' has been changed +-- so that it only works on 'Barrier', i.e. @PhasedBarrier ()@. This is because +-- phases haven't been modelled yet. +module Control.Concurrent.CHPSpec.Barriers (Barrier, EnrolledBarrier, newBarrier, newBarrierPri, newBarrierWithLabel, + PhasedBarrier, newPhasedBarrier, newPhasedBarrier', BarOpts(..), defaultIncPhase, defaultBarOpts, + barLabel, syncBarrier) where + +import Control.Monad.Trans + +import Control.Concurrent.CHPSpec.Base +import Control.Concurrent.CHPSpec.CSP + +type Barrier = PhasedBarrier () +type EnrolledBarrier = Enrolled PhasedBarrier () + +-- | Unlike normal CHP, this function only works on barriers with the unit type +-- for a phase. +syncBarrier :: EnrolledBarrier -> CHP () +syncBarrier (Enrolled (Barrier x)) = fakeCommBarr x + +data BarOpts phase = BarOpts { barIncPhase :: phase -> phase + , barPriority :: Int + , barOptsShow :: phase -> String + , barOptsLabel :: Maybe String } + +defaultIncPhase :: (Enum phase, Bounded phase, Eq phase) => phase -> phase +defaultIncPhase p + | p == maxBound = minBound + | otherwise = succ p + +defaultBarOpts :: (Enum phase, Bounded phase, Eq phase) => BarOpts phase +defaultBarOpts = BarOpts defaultIncPhase 0 (const "") Nothing + +barLabel :: (Enum phase, Bounded phase, Eq phase, Show phase) => String -> BarOpts phase +barLabel = BarOpts defaultIncPhase 0 show . Just + +newBarrier :: CHP Barrier +newBarrier = newBarrierPri 0 + +newBarrierPri :: Int -> CHP Barrier +newBarrierPri n = newPhasedBarrier' () $ BarOpts (const ()) n (const "") Nothing + +newPhasedBarrier :: (Enum phase, Bounded phase, Eq phase, Show phase) => phase -> CHP (PhasedBarrier phase) +newPhasedBarrier ph = newPhasedBarrier' ph $ BarOpts defaultIncPhase 0 show Nothing + +newPhasedBarrier' :: phase -> BarOpts phase -> CHP (PhasedBarrier phase) +newPhasedBarrier' _ o = do e <- lift newEvent + maybe (return ()) (lift . labelEvent e) $ barOptsLabel o + return $ Barrier e + +newBarrierWithLabel :: String -> CHP Barrier +newBarrierWithLabel = newPhasedBarrier' () . BarOpts (const ()) 0 (const "") . Just + diff --git a/Control/Concurrent/CHPSpec/Base.hs b/Control/Concurrent/CHPSpec/Base.hs new file mode 100644 --- /dev/null +++ b/Control/Concurrent/CHPSpec/Base.hs @@ -0,0 +1,125 @@ +-- Communicating Haskell Processes. +-- Copyright (c) 2008, University of Kent. +-- All rights reserved. +-- +-- Redistribution and use in source and binary forms, with or without +-- modification, are permitted provided that the following conditions are +-- met: +-- +-- * Redistributions of source code must retain the above copyright +-- notice, this list of conditions and the following disclaimer. +-- * Redistributions in binary form must reproduce the above copyright +-- notice, this list of conditions and the following disclaimer in the +-- documentation and/or other materials provided with the distribution. +-- * Neither the name of the University of Kent nor the names of its +-- contributors may be used to endorse or promote products derived from +-- this software without specific prior written permission. +-- +-- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +-- IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, +-- THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +-- PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +-- CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +-- EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +-- PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +-- PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +-- LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +-- NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +-- SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + + + +-- | A module containing various definitions relating to the CSP\/CSPPoison +-- monads, and poison. Not publicly visible. +module Control.Concurrent.CHPSpec.Base where + +import Control.Arrow +import Control.Monad (liftM) +import Control.Monad.State (StateT) +import Control.Monad.Trans (MonadTrans(..)) +import Data.Dynamic +import qualified Data.Map as Map +import qualified Data.Set as Set + +import Control.Concurrent.CHPSpec.Spec + +newtype CHPSpecT m a = CHPSpecT {runSpecT :: forall b. (a -> m (b, SpecMod)) -> m (b, SpecMod) } + +instance MonadTrans CHPSpecT where + lift m = CHPSpecT (m >>=) + +addSpecT1 :: forall m a. Monad m => m (a, SpecItem) -> CHPSpecT m a +addSpecT1 m = CHPSpecT $ \k -> m >>= apply k + where + apply :: (a -> m (b, SpecMod)) -> (a, SpecItem) -> m (b, SpecMod) + apply k (x, s) = liftM (second ((s :) .)) $ k x + +finSpecT :: Monad m => CHPSpecT m a -> m (a, Spec) +finSpecT = liftM (second finalise) . flip runSpecT (\x -> return (x, id)) + +stopSpecT :: Monad m => m SpecItem -> CHPSpecT m a +stopSpecT m = CHPSpecT $ const $ liftM (\sp -> (error "stopSpecT", (sp :))) m + +instance Monad m => Monad (CHPSpecT m) where + return x = CHPSpecT ($ x) + m >>= k = CHPSpecT $ \c -> runSpecT m $ \a -> runSpecT (k a) c + +newtype Enrolled b a = Enrolled (b a) deriving (Eq) + +instance Typeable (b a) => Typeable (Enrolled b a) where + typeOf x = let Enrolled b = Enrolled undefined `asTypeOf` x in mkTyConApp (mkTyCon "Enrolled") [typeOf b] + +type CheckArg = Dynamic -> Bool + +data CHPState = CHPState + { chpEventMap :: Map.Map Integer String + , chpIOEvents :: Set.Set Integer + , chpProcessMap :: Map.Map String (Map.Map Integer ([CheckArg], (Spec, Dynamic))) + , chpFreeNames :: [(Dynamic, CheckArg)] + , chpNextBottom :: !Integer + , chpNextProcess :: !Integer + } + +-- | The central monad of the library. You can use +-- the 'specify' function to model programs written with this monad. +type CHP = CHPSpecT (StateT CHPState IO) + +class Monad m => MonadCHP m where + liftCHP :: CHP a -> m a + +class Poisonable c where + poison :: MonadCHP m => c -> m () + checkForPoison :: MonadCHP m => c -> m () + +-- | Throws a poison exception. Poison is not currently modelled. +throwPoison :: CHP a +throwPoison = return $ error "throwPoison" -- checkPoison PoisonItem + +-- | Allows you to provide a handler for sections with poison. Since poison is +-- not currently modelled, this acts like 'const' at the moment. +onPoisonTrap :: forall a. CHP a -> CHP a -> CHP a +onPoisonTrap x _ = x + +-- | Like 'onPoisonTrap', this function allows you to provide a handler for +-- poison. Since poison is not currently modelled, this acts like 'const' at +-- the moment. +onPoisonRethrow :: CHP a -> CHP () -> CHP a +onPoisonRethrow x _ = x + +poisonAll :: (Poisonable c, MonadCHP m) => [c] -> m () +poisonAll = mapM_ poison + +instance MonadCHP CHP where + liftCHP = id + +altSpecT :: Monad m => [CHPSpecT m a] -> CHPSpecT m a +altSpecT ms = CHPSpecT $ + \k -> do xfs <- mapM (flip runSpecT k) ms + return (error "alt return", \s -> [Alt $ map (($ s) . snd) xfs]) + + +insertMapMap :: (Ord k, Ord k') => k -> k' -> v -> Map.Map k (Map.Map k' v) -> Map.Map k (Map.Map k' v) +insertMapMap k k' v = Map.insertWith Map.union k (Map.singleton k' v) + +collapseMapMap :: Ord kk => (k -> k' -> kk) -> Map.Map k (Map.Map k' v) -> Map.Map kk v +collapseMapMap f = Map.fromList . concatMap (\(k, kvs) -> map (first $ f k) kvs) . Map.toList . Map.map Map.toList diff --git a/Control/Concurrent/CHPSpec/CSP.hs b/Control/Concurrent/CHPSpec/CSP.hs new file mode 100644 --- /dev/null +++ b/Control/Concurrent/CHPSpec/CSP.hs @@ -0,0 +1,105 @@ +-- Communicating Haskell Processes. +-- Copyright (c) 2008, University of Kent. +-- All rights reserved. +-- +-- Redistribution and use in source and binary forms, with or without +-- modification, are permitted provided that the following conditions are +-- met: +-- +-- * Redistributions of source code must retain the above copyright +-- notice, this list of conditions and the following disclaimer. +-- * Redistributions in binary form must reproduce the above copyright +-- notice, this list of conditions and the following disclaimer in the +-- documentation and/or other materials provided with the distribution. +-- * Neither the name of the University of Kent nor the names of its +-- contributors may be used to endorse or promote products derived from +-- this software without specific prior written permission. +-- +-- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +-- IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, +-- THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +-- PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +-- CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +-- EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +-- PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +-- PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +-- LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +-- NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +-- SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + +-- | A module containing a few miscellaneous items that can't go in Control.Concurrent.CHP.Base +-- because they would form a cyclic module link. Not publicly visible. +-- TODO rename this module. +module Control.Concurrent.CHPSpec.CSP where + +import qualified Control.Exception as C +import Control.Monad.Reader +import Control.Monad.State +import qualified Data.List as L +import qualified Data.Map as Map +import Data.Typeable + +import Control.Concurrent.CHPSpec.Base +import Control.Concurrent.CHPSpec.Enroll +import Control.Concurrent.CHPSpec.Spec + +{- +-- | Synchronises on the given barrier. You must be enrolled on a barrier in order +-- to synchronise on it. Returns the new phase, following the synchronisation. +syncBarrierWith :: (Unique -> (Unique -> Integer) -> String -> [RecordedIndivEvent Unique]) + -> (Int -> STM ()) -> Enrolled PhasedBarrier phase -> CHP phase +syncBarrierWith recE storeN (Enrolled (Barrier (e,tv, fph))) + = buildOnEventPoison (wrapIndiv recE) e (EventActions incPhase (return ())) + (NoPoison <$> (atomically $ readTVar tv)) + where + incPhase :: Map.Map Unique Int -> STM () + incPhase m = do readTVar tv >>= writeTVar tv . fph + maybe (return ()) storeN $ Map.lookup (Event.getEventUnique e) m + +-} + +data PhasedBarrier phase = Barrier EventId + deriving (Eq, Typeable) + +instance Enrollable PhasedBarrier phase where + enroll b f + = f $ Enrolled b + resign _ m = m + +bottomPrefix :: String +bottomPrefix = "__CHP.bottom__" + +fakeCommIn :: Integer -> CHP a +fakeCommIn n = addSpecT1 $ do + st <- get + put $ st { chpNextBottom = succ $ chpNextBottom st } + return (error $ bottomPrefix ++ show (chpNextBottom st) + ,Sync $ Right (n, DirInput, chpNextBottom st) + ) + +fakeCommOut :: Integer -> a -> CHP () +fakeCommOut n x = addSpecT1 $ do + possErr <- lift $ C.try $ C.evaluate x + case possErr of + Left (C.ErrorCall s) | bottomPrefix `L.isPrefixOf` s + -> return ((), Sync $ Right + (n, DirOutput, read $ L.drop (L.length bottomPrefix) s)) + -- Wasn't one of our bottoms, we can't know anything about it, hope this will work in FDR: + _ -> return ((), Sync $ Left n) + +fakeCommBarr :: Integer -> CHP a +fakeCommBarr n = addSpecT1 $ return (undefined, Sync $ Left n) + +-- TODO this method will give a different channel each time, but at the moment +-- we treat it as if it will always act the same, so for example with recursive +-- processes (such as the sieve), it won't reflect the behaviour correctly +newEvent :: StateT CHPState IO EventId +newEvent = do st <- get + let n = toInteger $ Map.size $ chpEventMap st + put $ st { chpEventMap = Map.insert n "" $ chpEventMap st } + return n + +labelEvent :: EventId -> String -> StateT CHPState IO () +labelEvent n s = modify $ \st -> st { chpEventMap = Map.insert n s $ chpEventMap st } + +newtype Shared c a = Shared (c a) diff --git a/Control/Concurrent/CHPSpec/Channels.hs b/Control/Concurrent/CHPSpec/Channels.hs new file mode 100644 --- /dev/null +++ b/Control/Concurrent/CHPSpec/Channels.hs @@ -0,0 +1,55 @@ +-- Communicating Haskell Processes. +-- Copyright (c) 2008--2009, University of Kent. +-- All rights reserved. +-- +-- Redistribution and use in source and binary forms, with or without +-- modification, are permitted provided that the following conditions are +-- met: +-- +-- * Redistributions of source code must retain the above copyright +-- notice, this list of conditions and the following disclaimer. +-- * Redistributions in binary form must reproduce the above copyright +-- notice, this list of conditions and the following disclaimer in the +-- documentation and/or other materials provided with the distribution. +-- * Neither the name of the University of Kent nor the names of its +-- contributors may be used to endorse or promote products derived from +-- this software without specific prior written permission. +-- +-- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +-- IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, +-- THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +-- PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +-- CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +-- EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +-- PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +-- PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +-- LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +-- NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +-- SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + + +-- | The module containing all the different types of channels in CHP. +-- +-- See +-- for details of modelling communication. +module Control.Concurrent.CHPSpec.Channels ( + -- * Channel Creation and Types + module Control.Concurrent.CHPSpec.Channels.Creation, + -- * Channel-Ends + module Control.Concurrent.CHPSpec.Channels.Ends, + + -- * Reading and Writing with Channels + module Control.Concurrent.CHPSpec.Channels.Communication, + + -- * Useful Type and Function Synonyms + module Control.Concurrent.CHPSpec.Channels.Synonyms + + ) + where + + +import Control.Concurrent.CHPSpec.Channels.Base +import Control.Concurrent.CHPSpec.Channels.Communication +import Control.Concurrent.CHPSpec.Channels.Creation +import Control.Concurrent.CHPSpec.Channels.Ends +import Control.Concurrent.CHPSpec.Channels.Synonyms diff --git a/Control/Concurrent/CHPSpec/Channels/Base.hs b/Control/Concurrent/CHPSpec/Channels/Base.hs new file mode 100644 --- /dev/null +++ b/Control/Concurrent/CHPSpec/Channels/Base.hs @@ -0,0 +1,65 @@ +-- Communicating Haskell Processes. +-- Copyright (c) 2008--2009, University of Kent. +-- All rights reserved. +-- +-- Redistribution and use in source and binary forms, with or without +-- modification, are permitted provided that the following conditions are +-- met: +-- +-- * Redistributions of source code must retain the above copyright +-- notice, this list of conditions and the following disclaimer. +-- * Redistributions in binary form must reproduce the above copyright +-- notice, this list of conditions and the following disclaimer in the +-- documentation and/or other materials provided with the distribution. +-- * Neither the name of the University of Kent nor the names of its +-- contributors may be used to endorse or promote products derived from +-- this software without specific prior written permission. +-- +-- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +-- IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, +-- THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +-- PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +-- CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +-- EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +-- PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +-- PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +-- LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +-- NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +-- SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + +module Control.Concurrent.CHPSpec.Channels.Base where + +import Control.Arrow ((&&&)) +import Control.Monad +import Control.Monad.Trans +import Data.Typeable + +import Control.Concurrent.CHPSpec.Base +import Control.Concurrent.CHPSpec.CSP +import Control.Concurrent.CHPSpec.Spec + +newtype Chanin a = Chanin (STMChannel a) deriving (Eq, Typeable) + +newtype Chanout a = Chanout (STMChannel a) deriving (Eq, Typeable) + +newtype STMChannel a = STMChan EventId + deriving (Eq, Typeable) + +data Chan r w a = Chan { + -- | Gets the channel's identifier. Useful if you need to be able to identify + -- a channel in the trace later on. + getChannelIdentifier :: EventId, + reader :: r a, + writer :: w a} + +instance Poisonable (Chanin a) where + poison (Chanin _) = return () + checkForPoison (Chanin _) = return () + +instance Poisonable (Chanout a) where + poison (Chanout _) = return () + checkForPoison (Chanout _) = return () + +stmChannel :: MonadCHP m => m (EventId, STMChannel a) +stmChannel = liftM (id &&& STMChan) $ liftCHP $ lift newEvent + diff --git a/Control/Concurrent/CHPSpec/Channels/Communication.hs b/Control/Concurrent/CHPSpec/Channels/Communication.hs new file mode 100644 --- /dev/null +++ b/Control/Concurrent/CHPSpec/Channels/Communication.hs @@ -0,0 +1,90 @@ +-- Communicating Haskell Processes. +-- Copyright (c) 2008--2009, University of Kent. +-- All rights reserved. +-- +-- Redistribution and use in source and binary forms, with or without +-- modification, are permitted provided that the following conditions are +-- met: +-- +-- * Redistributions of source code must retain the above copyright +-- notice, this list of conditions and the following disclaimer. +-- * Redistributions in binary form must reproduce the above copyright +-- notice, this list of conditions and the following disclaimer in the +-- documentation and/or other materials provided with the distribution. +-- * Neither the name of the University of Kent nor the names of its +-- contributors may be used to endorse or promote products derived from +-- this software without specific prior written permission. +-- +-- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +-- IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, +-- THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +-- PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +-- CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +-- EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +-- PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +-- PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +-- LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +-- NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +-- SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + +module Control.Concurrent.CHPSpec.Channels.Communication ( + ReadableChannel(..), WriteableChannel(..), writeValue, writeChannelStrict + ) where + +import Control.DeepSeq +import Control.Monad + +import Control.Concurrent.CHPSpec.Base +import Control.Concurrent.CHPSpec.CSP +import Control.Concurrent.CHPSpec.Channels.Base + +class ReadableChannel chanEnd where -- minimal implementation: extReadChannel + readChannel :: chanEnd a -> CHP a + readChannel c = extReadChannel c return + -- | Currently, extended inputs and outputs are modelled (incorrectly) as standard + -- inputs and outputs. + extReadChannel :: chanEnd a -> (a -> CHP b) -> CHP b + +class WriteableChannel chanEnd where -- minimal implementation: extWriteChannel + writeChannel :: chanEnd a -> a -> CHP () + writeChannel c x = extWriteChannel c (return x) >> return () + + -- | Currently, extended inputs and outputs are modelled (incorrectly) as standard + -- inputs and outputs. + extWriteChannel :: chanEnd a -> CHP a -> CHP () + extWriteChannel c = extWriteChannel' c . liftM (flip (,) ()) + + -- | Currently, extended inputs and outputs are modelled (incorrectly) as standard + -- inputs and outputs. + extWriteChannel' :: chanEnd a -> CHP (a, b) -> CHP b + + +-- ========== +-- Functions: +-- ========== + +writeValue :: WriteableChannel chanEnd => a -> chanEnd a -> CHP () +writeValue = flip writeChannel + +-- | This function strictly evaluates its second argument and then behaves like +-- 'writeChannel'. +writeChannelStrict :: (NFData a, WriteableChannel chanEnd) => chanEnd a -> a -> CHP () +writeChannelStrict c x = case rnf x of () -> writeChannel c x + +-- ========== +-- Instances: +-- ========== + +instance ReadableChannel Chanin where + readChannel (Chanin (STMChan c)) = fakeCommIn c + + extReadChannel (Chanin (STMChan c)) body + = fakeCommIn c >>= body + +instance WriteableChannel Chanout where + writeChannel (Chanout (STMChan c)) x + = fakeCommOut c x >> return () + extWriteChannel (Chanout (STMChan c)) body + = body >>= fakeCommOut c >> return () + extWriteChannel' (Chanout (STMChan c)) body + = body >>= \(val, ret) -> fakeCommOut c val >> return ret diff --git a/Control/Concurrent/CHPSpec/Channels/Creation.hs b/Control/Concurrent/CHPSpec/Channels/Creation.hs new file mode 100644 --- /dev/null +++ b/Control/Concurrent/CHPSpec/Channels/Creation.hs @@ -0,0 +1,116 @@ +-- Communicating Haskell Processes. +-- Copyright (c) 2008--2009, University of Kent. +-- All rights reserved. +-- +-- Redistribution and use in source and binary forms, with or without +-- modification, are permitted provided that the following conditions are +-- met: +-- +-- * Redistributions of source code must retain the above copyright +-- notice, this list of conditions and the following disclaimer. +-- * Redistributions in binary form must reproduce the above copyright +-- notice, this list of conditions and the following disclaimer in the +-- documentation and/or other materials provided with the distribution. +-- * Neither the name of the University of Kent nor the names of its +-- contributors may be used to endorse or promote products derived from +-- this software without specific prior written permission. +-- +-- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +-- IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, +-- THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +-- PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +-- CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +-- EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +-- PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +-- PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +-- LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +-- NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +-- SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + +module Control.Concurrent.CHPSpec.Channels.Creation ( + Chan, Channel(..), newChannel, ChanOpts(..), defaultChanOpts, chanLabel, newChannelWR, newChannelRW, + newChannelList, newChannelListWithLabels, newChannelListWithStem, + labelChannel + ) where + +import Control.Monad +import Control.Monad.Trans + +import Control.Concurrent.CHPSpec.Base +import Control.Concurrent.CHPSpec.Channels.Base +import Control.Concurrent.CHPSpec.CSP +import Control.Concurrent.CHPSpec.Spec + +class Channel r w where + newChannel' :: MonadCHP m => ChanOpts a -> m (Chan r w a) + sameChannel :: r a -> w a -> Bool + +-- | Options for channel creation. The first two will be ignored, but the label +-- (if present) will be used to label the channel in the specification. +data ChanOpts a = ChanOpts { + chanOptsPriority :: Int, + chanOptsShow :: a -> String, + chanOptsLabel :: Maybe String } + +defaultChanOpts :: ChanOpts a +defaultChanOpts = ChanOpts 0 (const "") Nothing + +chanLabel :: Show a => String -> ChanOpts a +chanLabel = ChanOpts 0 show . Just + +newChannel :: (MonadCHP m, Channel r w) => m (Chan r w a) +newChannel = newChannel' defaultChanOpts + +newChannelRW :: (Channel r w, MonadCHP m) => m (r a, w a) +newChannelRW = do c <- newChannel + return (reader c, writer c) + +newChannelWR :: (Channel r w, MonadCHP m) => m (w a, r a) +newChannelWR = do c <- newChannel + return (writer c, reader c) + +newChannelList :: (Channel r w, MonadCHP m) => Int -> m [Chan r w a] +newChannelList n = replicateM n newChannel + +newChannelListWithStem :: (Channel r w, MonadCHP m) => Int -> String -> m [Chan r w a] +newChannelListWithStem n s = sequence [newChannel' $ ChanOpts 0 (const "") (Just $ s ++ show i) | i <- [0 .. (n - 1)]] + +newChannelListWithLabels :: (Channel r w, MonadCHP m) => [String] -> m [Chan r w a] +newChannelListWithLabels = mapM (newChannel' . ChanOpts 0 (const "") . Just) + + +-- | Labels a channel in the traces. It is easiest to do this at creation. +-- The effect of re-labelling channels after their first use is undefined. +-- +-- This function does work as expected in chp-spec. +labelChannel :: MonadCHP m => Chan r w a -> String -> m () +labelChannel c = liftCHP . lift . labelEvent (getChannelIdentifier c) + + +instance Channel Chanin Chanout where + newChannel' o = do c <- chan (stmChannel) Chanin Chanout + maybe (return ()) (labelChannel c) (chanOptsLabel o) + return c + sameChannel (Chanin x) (Chanout y) = x == y + +instance Channel (Shared Chanin) Chanout where + newChannel' o = do + c <- newChannel' o + return $ Chan (getChannelIdentifier c) (Shared (reader c)) (writer c) + sameChannel (Shared (Chanin x)) (Chanout y) = x == y + +instance Channel Chanin (Shared Chanout) where + newChannel' o = do + c <- newChannel' o + return $ Chan (getChannelIdentifier c) (reader c) (Shared (writer c)) + sameChannel (Chanin x) (Shared (Chanout y)) = x == y + +instance Channel (Shared Chanin) (Shared Chanout) where + newChannel' o = do + c <- newChannel' o + return $ Chan (getChannelIdentifier c) (Shared (reader c)) (Shared (writer c)) + sameChannel (Shared (Chanin x)) (Shared (Chanout y)) = x == y + +chan :: Monad m => m (EventId, c a) -> (c a -> r a) -> (c a -> w a) -> m (Chan r w a) +chan m r w = do (u, x) <- m + return $ Chan u (r x) (w x) diff --git a/Control/Concurrent/CHPSpec/Channels/Ends.hs b/Control/Concurrent/CHPSpec/Channels/Ends.hs new file mode 100644 --- /dev/null +++ b/Control/Concurrent/CHPSpec/Channels/Ends.hs @@ -0,0 +1,46 @@ +-- Communicating Haskell Processes. +-- Copyright (c) 2008--2009, University of Kent. +-- All rights reserved. +-- +-- Redistribution and use in source and binary forms, with or without +-- modification, are permitted provided that the following conditions are +-- met: +-- +-- * Redistributions of source code must retain the above copyright +-- notice, this list of conditions and the following disclaimer. +-- * Redistributions in binary form must reproduce the above copyright +-- notice, this list of conditions and the following disclaimer in the +-- documentation and/or other materials provided with the distribution. +-- * Neither the name of the University of Kent nor the names of its +-- contributors may be used to endorse or promote products derived from +-- this software without specific prior written permission. +-- +-- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +-- IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, +-- THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +-- PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +-- CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +-- EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +-- PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +-- PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +-- LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +-- NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +-- SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + +module Control.Concurrent.CHPSpec.Channels.Ends ( + Chanin, Chanout, Shared, + reader, writer, readers, writers, + claim) where + +import Control.Concurrent.CHPSpec.Base +import Control.Concurrent.CHPSpec.CSP +import Control.Concurrent.CHPSpec.Channels.Base + +readers :: [Chan r w a] -> [r a] +readers = map reader + +writers :: [Chan r w a] -> [w a] +writers = map writer + +claim :: Shared c a -> (c a -> CHP b) -> CHP b +claim (Shared c) body = body c diff --git a/Control/Concurrent/CHPSpec/Channels/Synonyms.hs b/Control/Concurrent/CHPSpec/Channels/Synonyms.hs new file mode 100644 --- /dev/null +++ b/Control/Concurrent/CHPSpec/Channels/Synonyms.hs @@ -0,0 +1,68 @@ +-- Communicating Haskell Processes. +-- Copyright (c) 2008--2009, University of Kent. +-- All rights reserved. +-- +-- Redistribution and use in source and binary forms, with or without +-- modification, are permitted provided that the following conditions are +-- met: +-- +-- * Redistributions of source code must retain the above copyright +-- notice, this list of conditions and the following disclaimer. +-- * Redistributions in binary form must reproduce the above copyright +-- notice, this list of conditions and the following disclaimer in the +-- documentation and/or other materials provided with the distribution. +-- * Neither the name of the University of Kent nor the names of its +-- contributors may be used to endorse or promote products derived from +-- this software without specific prior written permission. +-- +-- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +-- IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, +-- THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +-- PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +-- CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +-- EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +-- PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +-- PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +-- LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +-- NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +-- SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + +module Control.Concurrent.CHPSpec.Channels.Synonyms ( + OneToOneChannel, oneToOneChannel, oneToOneChannel', + OneToAnyChannel, oneToAnyChannel, oneToAnyChannel', + AnyToOneChannel, anyToOneChannel, anyToOneChannel', + AnyToAnyChannel, anyToAnyChannel, anyToAnyChannel' + ) where + +import Control.Concurrent.CHPSpec.Base +import Control.Concurrent.CHPSpec.Channels.Creation +import Control.Concurrent.CHPSpec.Channels.Ends + +type OneToOneChannel = Chan Chanin Chanout +type AnyToOneChannel = Chan (Chanin) (Shared Chanout) +type OneToAnyChannel = Chan (Shared Chanin) (Chanout) +type AnyToAnyChannel = Chan (Shared Chanin) (Shared Chanout) + +oneToOneChannel :: MonadCHP m => m (OneToOneChannel a) +oneToOneChannel = newChannel + +oneToOneChannel' :: MonadCHP m => ChanOpts a -> m (OneToOneChannel a) +oneToOneChannel' = newChannel' + +anyToOneChannel :: MonadCHP m => m (AnyToOneChannel a) +anyToOneChannel = newChannel + +oneToAnyChannel :: MonadCHP m => m (OneToAnyChannel a) +oneToAnyChannel = newChannel + +anyToAnyChannel :: MonadCHP m => m (AnyToAnyChannel a) +anyToAnyChannel = newChannel + +anyToOneChannel' :: MonadCHP m => ChanOpts a -> m (AnyToOneChannel a) +anyToOneChannel' = newChannel' + +oneToAnyChannel' :: MonadCHP m => ChanOpts a -> m (OneToAnyChannel a) +oneToAnyChannel' = newChannel' + +anyToAnyChannel' :: MonadCHP m => ChanOpts a -> m (AnyToAnyChannel a) +anyToAnyChannel' = newChannel' diff --git a/Control/Concurrent/CHPSpec/Enroll.hs b/Control/Concurrent/CHPSpec/Enroll.hs new file mode 100644 --- /dev/null +++ b/Control/Concurrent/CHPSpec/Enroll.hs @@ -0,0 +1,70 @@ +-- Communicating Haskell Processes. +-- Copyright (c) 2008, University of Kent. +-- All rights reserved. +-- +-- Redistribution and use in source and binary forms, with or without +-- modification, are permitted provided that the following conditions are +-- met: +-- +-- * Redistributions of source code must retain the above copyright +-- notice, this list of conditions and the following disclaimer. +-- * Redistributions in binary form must reproduce the above copyright +-- notice, this list of conditions and the following disclaimer in the +-- documentation and/or other materials provided with the distribution. +-- * Neither the name of the University of Kent nor the names of its +-- contributors may be used to endorse or promote products derived from +-- this software without specific prior written permission. +-- +-- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +-- IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, +-- THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +-- PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +-- CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +-- EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +-- PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +-- PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +-- LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +-- NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +-- SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + +-- | A module with support for things that are enrollable. +-- +-- Enrollment is currently pretty much ignored during model generation, but these +-- operations are provided so that you don't have to change your program. +module Control.Concurrent.CHPSpec.Enroll (Enrolled, Enrollable(..), furtherEnroll, + enrollPair, enrollList, enrollAll, enrollAll_, enrollAllT, enrollOneMany) where + +import Control.Concurrent.CHPSpec.Base +import Control.Concurrent.CHPSpec.Parallel + +class Enrollable b z where + enroll :: b z -> (Enrolled b z -> CHP a) -> CHP a + resign :: Enrolled b z -> CHP a -> CHP a + +furtherEnroll :: Enrollable b z => Enrolled b z -> (Enrolled b z -> CHP a) -> CHP a +furtherEnroll (Enrolled x) = enroll x + +enrollPair :: (Enrollable b p, Enrollable b' p') => (b p, b' p') -> ((Enrolled + b p, Enrolled b' p') -> CHP a) -> CHP a +enrollPair (b0,b1) f = enroll b0 $ \eb0 -> enroll b1 $ \eb1 -> f (eb0, eb1) + +enrollList :: Enrollable b p => [b p] -> ([Enrolled b p] -> CHP a) -> CHP a +enrollList [] f = f [] +enrollList (b:bs) f = enroll b $ \eb -> enrollList bs $ f . (eb:) + +enrollAll :: Enrollable b p => CHP (b p) -> [Enrolled b p -> CHP a] -> CHP [a] +enrollAll = enrollAllT runParallel + +enrollAllT :: Enrollable b p => ([a] -> CHP c) -> CHP (b p) -> [Enrolled b p -> a] -> CHP c +enrollAllT run mbar ps = mbar >>= flip enrollList (run . zipWith ($) ps) . replicate (length ps) + +enrollOneMany :: Enrollable b p => ([Enrolled b p] -> CHP a) -> [(CHP (b p), Enrolled b p -> CHP c)] -> CHP (a, [c]) +enrollOneMany p [] = p [] >>= \x -> return (x, []) +enrollOneMany p ((mbar, q) : rest) + = do bar <- mbar + enrollPair (bar, bar) $ \(b0, b1) -> + do ((p', q'), rest') <- enrollOneMany (\bs -> p (b0:bs) <||> q b1) rest + return (p', q' : rest') + +enrollAll_ :: Enrollable b p => CHP (b p) -> [Enrolled b p -> CHP a] -> CHP () +enrollAll_ = enrollAllT runParallel_ diff --git a/Control/Concurrent/CHPSpec/LazySmallCheck.hs b/Control/Concurrent/CHPSpec/LazySmallCheck.hs new file mode 100644 --- /dev/null +++ b/Control/Concurrent/CHPSpec/LazySmallCheck.hs @@ -0,0 +1,235 @@ +-- | This module is a near-copy of the Test.LazySmallCheck module from the lazysmallcheck +-- package on Hackage. It was written by Matthew Naylor and Fredrik Lindblad. +-- I have modified it to add the 'fuzz' function that is used by chp-spec internally, +-- but to write that function I needed access to more internals than the original +-- Test.LazySmallCheck exposed, hence I had to make a copy of the module. Unfortunately, +-- this means that the Serial type-class here is a different type-class (despite +-- being identical in behaviour and API) from the original lazysmallcheck package. +-- The modified module is exposed in case you need to supply any of your own instances +-- for 'Serial'. For more explanation of how Lazy SmallCheck is used in this library +-- for modelling IO actions, see this blog post: +module Control.Concurrent.CHPSpec.LazySmallCheck + ( Serial(series) -- :: class + , Series -- :: type Series a = Int -> Cons a + , Cons -- :: * + , cons -- :: a -> Series a + , (><) -- :: Series (a -> b) -> Series a -> Series b + , (\/) -- :: Series a -> Series a -> Series a + , drawnFrom -- :: [a] -> Cons a + , cons0 -- :: a -> Series a + , cons1 -- :: Serial a => (a -> b) -> Series b + , cons2 -- :: (Serial a, Serial b) => (a -> b -> c) -> Series c + , cons3 -- :: ... + , cons4 -- :: ... + , cons5 -- :: ... + , fuzz + ) + where + +import Control.Applicative ((<$>)) +import Control.Arrow +import Control.Exception +import Control.Monad.State + +infixr 3 \/ +infixl 4 >< + +type Pos = [Int] + +data Term = Var Pos Type | Ctr Int [Term] + +data Type = SumOfProd [[Type]] + +type Series a = Int -> Cons a + +data Cons a = C Type ([[Term] -> a]) Bool + +class Serial a where + series :: Series a + +-- Series constructors + +cons :: a -> Series a +cons a d = C (SumOfProd [[]]) [const a] True + +(><) :: Series (a -> b) -> Series a -> Series b +(f >< a) d = C (SumOfProd [ta:p | shallow, p <- ps]) cs (shallow && fComplete && aComplete) + where + C (SumOfProd ps) cfs fComplete = f d + C ta cas aComplete = a (d-1) + cs = [\(x:xs) -> cf xs (conv cas x) | shallow, cf <- cfs] + shallow = d > 0 && nonEmpty ta + +nonEmpty :: Type -> Bool +nonEmpty (SumOfProd ps) = not (null ps) + +(\/) :: Series a -> Series a -> Series a +(a \/ b) d = C (SumOfProd (ssa ++ ssb)) (ca ++ cb) (aComplete && bComplete) + where + C (SumOfProd ssa) ca aComplete = a d + C (SumOfProd ssb) cb bComplete = b d + +conv :: [[Term] -> a] -> Term -> a +conv cs (Var p _) = error ('\0':map toEnum p) +conv cs (Ctr i xs) = (cs !! i) xs + +drawnFrom :: [a] -> Cons a +drawnFrom xs = C (SumOfProd (map (const []) xs)) (map const xs) False + +-- Helpers, a la SmallCheck + +cons0 :: a -> Series a +cons0 f = cons f + +cons1 :: Serial a => (a -> b) -> Series b +cons1 f = cons f >< series + +cons2 :: (Serial a, Serial b) => (a -> b -> c) -> Series c +cons2 f = cons f >< series >< series + +cons3 :: (Serial a, Serial b, Serial c) => (a -> b -> c -> d) -> Series d +cons3 f = cons f >< series >< series >< series + +cons4 :: (Serial a, Serial b, Serial c, Serial d) => + (a -> b -> c -> d -> e) -> Series e +cons4 f = cons f >< series >< series >< series >< series + +cons5 :: (Serial a, Serial b, Serial c, Serial d, Serial e) => + (a -> b -> c -> d -> e -> f) -> Series f +cons5 f = cons f >< series >< series >< series >< series >< series + +-- Standard instances + +instance Serial () where + series = cons0 () + +instance Serial Bool where + series = cons0 False \/ cons0 True + +instance Serial a => Serial (Maybe a) where + series = cons0 Nothing \/ cons1 Just + +instance (Serial a, Serial b) => Serial (Either a b) where + series = cons1 Left \/ cons1 Right + +instance Serial a => Serial [a] where + series = cons0 [] \/ cons2 (:) + +instance (Serial a, Serial b) => Serial (a, b) where + series = cons2 (,) . (+1) + +instance (Serial a, Serial b, Serial c) => Serial (a, b, c) where + series = cons3 (,,) . (+1) + +instance (Serial a, Serial b, Serial c, Serial d) => + Serial (a, b, c, d) where + series = cons4 (,,,) . (+1) + +instance (Serial a, Serial b, Serial c, Serial d, Serial e) => + Serial (a, b, c, d, e) where + series = cons5 (,,,,) . (+1) + +instance Serial Int where + series d = drawnFrom [-d..d] + +instance Serial Integer where + series d = drawnFrom (map toInteger [-d..d]) + +instance Serial Char where + series d = drawnFrom (take (d+1) ['a'..]) + +instance Serial Float where + series d = drawnFrom (floats d) + +instance Serial Double where + series d = drawnFrom (floats d) + +floats :: RealFloat a => Int -> [a] +floats d = [ encodeFloat sig exp + | sig <- map toInteger [-d..d] + , exp <- [-d..d] + , odd sig || sig == 0 && exp == 0 + ] + +-- Term refinement + +refine :: Term -> Pos -> [Term] +refine (Var p (SumOfProd ss)) [] = new p ss +refine (Ctr c xs) p = map (Ctr c) (refineList xs p) + +refineList :: [Term] -> Pos -> [[Term]] +refineList xs (i:is) = [ls ++ y:rs | y <- refine x is] + where (ls, x:rs) = splitAt i xs + +new :: Pos -> [[Type]] -> [Term] +new p ps = [ Ctr c (zipWith (\i t -> Var (p++[i]) t) [0..] ts) + | (c, ts) <- zip [0..] ps ] + +-- Find total instantiations of a partial value + +total :: Term -> [Term] +total val = tot val + where + tot (Ctr c xs) = [Ctr c ys | ys <- mapM tot xs] + tot (Var p (SumOfProd ss)) = [y | x <- new p ss, y <- tot x] + +-- Answers + +answer :: IO a -> (a -> IO b) -> (Pos -> IO b) -> IO b +answer a known unknown = + do res <- try a + case res of + Right b -> known b + Left (ErrorCall ('\0':p)) -> unknown (map fromEnum p) + Left e -> throw e + +resultVal :: forall b s. Result s b -> StateT s IO ([b], Bool) +resultVal r = ref (args r) + where + ref :: [Term] -> StateT s IO ([b], Bool) + ref xs = StateT $ \s -> answer (flip runStateT s $ apply r xs) (\(x, s) -> return (([x], complete r), s)) (unknown s) + where + unknown :: s -> Pos -> IO (([b], Bool), s) + unknown s p = (first $ (concat *** and) . unzip) <$> (flip runStateT s $ mapM ref (refineList xs p)) + +data Result s b = + Result { args :: [Term] + , apply :: [Term] -> StateT s IO b + , complete :: Bool + } + +--data P b = P (Int -> Int -> Result b) + +runEnd :: ([Term] -> StateT s IO r) -> Int -> Int -> Result s r +runEnd f _ _ = Result [] (f . reverse) True + +runParam :: Serial a => ([Term] -> a -> StateT s IO r) -> Int -> Int -> Result s r +runParam f n d = + let C t c comp = series d + c' = conv c + r = runEnd (\(x:xs) -> f xs (c' x)) (n+1) d + in r { args = Var [n] t : args r, complete = complete r && comp } + +-- Top-level interface + +depthCheck :: Serial a => Int -> (a -> StateT s IO r) -> StateT s IO ([r], Bool) +depthCheck d p = resultVal $ runParam (const p) 0 d + +smallCheck :: Serial a => Int -> (a -> StateT s IO r) -> StateT s IO ([r], Bool) +smallCheck d p = smallCheck' [] 0 + where + -- Should I accumulate prev? I think later depths subsume earlier ones... + smallCheck' prev n + | n <= d = do (xs, comp) <- depthCheck n p + if comp + then return (xs, True) + else smallCheck' xs (succ n) + | otherwise = return (prev, False) + +--test :: Testable a r => a -> IO () +--test p = mapM_ (`depthCheck` p) [0..] + +-- Finds all possible behaviours of the code block: +fuzz :: (Serial a) => (a -> StateT s IO b) -> StateT s IO ([b], Bool) +fuzz = smallCheck 10 + diff --git a/Control/Concurrent/CHPSpec/Monad.hs b/Control/Concurrent/CHPSpec/Monad.hs new file mode 100644 --- /dev/null +++ b/Control/Concurrent/CHPSpec/Monad.hs @@ -0,0 +1,179 @@ +-- Communicating Haskell Processes. +-- Copyright (c) 2008, University of Kent. +-- All rights reserved. +-- +-- Redistribution and use in source and binary forms, with or without +-- modification, are permitted provided that the following conditions are +-- met: +-- +-- * Redistributions of source code must retain the above copyright +-- notice, this list of conditions and the following disclaimer. +-- * Redistributions in binary form must reproduce the above copyright +-- notice, this list of conditions and the following disclaimer in the +-- documentation and/or other materials provided with the distribution. +-- * Neither the name of the University of Kent nor the names of its +-- contributors may be used to endorse or promote products derived from +-- this software without specific prior written permission. +-- +-- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +-- IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, +-- THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +-- PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +-- CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +-- EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +-- PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +-- PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +-- LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +-- NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +-- SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + +-- | This module contains all the central monads in the CHP library. +module Control.Concurrent.CHPSpec.Monad + ( + -- * CHP Monad + CHP, MonadCHP(..), liftIO_CHP, liftIO_CHP', foreverP, specify, Process, process, subProcess, + + onPoisonTrap, onPoisonRethrow, throwPoison, Poisonable(..), poisonAll, + + -- * Primitive actions + skip, stop --, waitFor + ) where + +import Control.Applicative ((<$>)) +import Control.Arrow +import Control.Monad.Reader +import Control.Monad.State +import qualified Data.Foldable as F (toList) +import Data.Function (on) +import Data.List (intercalate, nubBy) +import qualified Data.Map as Map +import Data.Maybe +import qualified Data.Set as Set +import qualified Data.Traversable as T +import qualified Text.PrettyPrint.HughesPJ as PP + +-- This module primarily re-exports the public definitions from +-- Control.Concurrent.CHP.{Base,CSP,Poison}: + +import Control.Concurrent.CHPSpec.Base +import Control.Concurrent.CHPSpec.CSP +import Control.Concurrent.CHPSpec.LazySmallCheck +import Control.Concurrent.CHPSpec.Print +import Control.Concurrent.CHPSpec.Process +import Control.Concurrent.CHPSpec.Spec + +-- | Models processes that run forever. +-- +-- Anything following a 'foreverP' call in sequence will not be modelled. +foreverP :: CHP a -> CHP b +foreverP = stopSpecT . liftM (Repeat . snd) . finSpecT + +skip :: CHP () +skip = return () + +stop :: CHP a +stop = stopSpecT $ return Stop + +-- | Like fromMaybe, but treats Just "" like Nothing +fromMaybeStr :: String -> Maybe String -> String +fromMaybeStr def m = case m of + Just str | not (null str) -> str + _ -> def + +-- | Repeatedly applies the given function to the contents of the map until it +-- no longer changes +iter :: (Eq events, Ord k) => (Map.Map k events -> spec -> events) -> (Map.Map k (spec, events)) -> (Map.Map k (spec, events)) +iter f m = let m' = Map.map ((id &&& f (Map.map snd m)) . fst) m + in if Map.map snd m == Map.map snd m' + then m' + else iter f m' + +-- | The top-level function in this library, to be used in place of runCHP in your +-- program. You pass it a boolean (True if you want to leave the dummy IO events +-- exposed, False if you want them hidden) and a CHP process that you want to specify. +-- The result is a String containing a CSP-M specification that can be written +-- out to a file and read in to other tools, such as FDR, PRoBE and others. +specify :: Bool -> CHP () -> IO String +specify showIO main + = specify' showIO <$> execStateT (finSpecT $ process "main" main) emptyCHPState + where + emptyCHPState = CHPState Map.empty Set.empty Map.empty [] 1 1 + +specify' :: Bool -> CHPState -> String +specify' showIO st = render specs ++ declMain + where + render :: Map.Map String [SpecItem' String String] -> String + render = PP.render . PP.vcat . (map pprintForwardDecl allChans ++) . map (pprintProc eventMap) . Map.toList + + declMain :: String + declMain = "\nmain = main_1 " ++ (if showIO then "" else + "\\ {" ++ intercalate "," (map getName $ Set.toList $ chpIOEvents st) ++ "}" + ) ++ "\n" + where + getName = fromJust . flip Map.lookup events + + pulledProcesses :: Map.Map (Integer, String) [SpecItem] + pulledProcesses = + collapseMapMap (\s n -> (n, s ++ "_" ++ show n)) + (Map.unionWith Map.union oldProcs pulledProcs) + where + rawProcesses :: Map.Map String (Map.Map Integer Spec) + rawProcesses = Map.map (Map.map (fst . snd)) $ chpProcessMap st + + rep :: Spec -> State (Integer, Map.Map String (Map.Map Integer Spec)) Integer + rep x = do (!n, m) <- get + put (succ n, insertMapMap "repeated" n (x ++ [Call n]) m) + return n + + oldProcs, pulledProcs :: Map.Map String (Map.Map Integer Spec) + (oldProcs, (_, pulledProcs)) + = runState (T.mapM (T.mapM $ T.mapM $ pullUpRepeatM rep) rawProcesses) + (chpNextProcess st, Map.empty) + + specs :: Map.Map String [SpecItem' String String] + specs = Map.mapKeys snd $ Map.map (fmap (subSpec showProc showComm) . pruneSpec) pulledProcesses + where + showProc :: ProcessId -> String + showProc p = fromMaybeStr ("p_" ++ show p) $ Map.lookup p procs + + showComm :: CommId -> String + showComm (Left c) = fromMaybeStr ("c_" ++ show c) $ Map.lookup c events + showComm (Right (c, d, x)) = showComm (Left c) ++ (if d == DirInput + then "?" else "!") ++ "x_" ++ show x + + procs = Map.fromList $ Map.keys pulledProcesses + + allChans = nubBy ((==) `on` baseName) $ F.toList $ foldr Set.union Set.empty $ Map.elems eventMap + + events = chpEventMap st + + eventMap = Map.map snd $ iter (findAllComms baseName) $ Map.map (flip (,) Set.empty) $ specs + + baseName = takeWhile (`notElem` "?!.") + +-- | Models the lifting of an IO action into the CHP monad. +-- +-- The IO computation itself is completely ignored. The label (first parameter) +-- is used to label various different dummy events, which arise from exploring +-- the return type of the IO computation. To support this exploration, the return +-- type must be an instance of 'Serial'. +-- +-- More details and a full explanation of how IO events are modelled are available +-- in this blog post: +liftIO_CHP' :: Serial a => String -> IO a -> CHP a +liftIO_CHP' label _ = CHPSpecT $ \k -> + do (vals, complete) <- fuzz k + unless complete $ + liftIO $ putStrLn "Incomplete fuzzing of IO computation" + nonces <- replicateM (length vals) newEvent + let firstLabel = "IO_" ++ label ++ show (head nonces) + zipWithM_ labelEvent nonces (map (firstLabel++) suffixes) + modify $ \st -> st { chpIOEvents = Set.union + (Set.fromList nonces) (chpIOEvents st) } + return (error "liftIO return", \s -> [Alt $ zipWith (\n f -> Sync (Left n) : snd f s) nonces vals]) + where + suffixes = map (:[]) ['A'..'Z'] ++ map show [(0::Integer)..] + +-- | Like @liftIO_CHP'@, but with an empty label. +liftIO_CHP :: Serial a => IO a -> CHP a +liftIO_CHP = liftIO_CHP' "" diff --git a/Control/Concurrent/CHPSpec/Parallel.hs b/Control/Concurrent/CHPSpec/Parallel.hs new file mode 100644 --- /dev/null +++ b/Control/Concurrent/CHPSpec/Parallel.hs @@ -0,0 +1,74 @@ +-- Communicating Haskell Processes. +-- Copyright (c) 2008-2010, University of Kent, Neil Brown. +-- All rights reserved. +-- +-- Redistribution and use in source and binary forms, with or without +-- modification, are permitted provided that the following conditions are +-- met: +-- +-- * Redistributions of source code must retain the above copyright +-- notice, this list of conditions and the following disclaimer. +-- * Redistributions in binary form must reproduce the above copyright +-- notice, this list of conditions and the following disclaimer in the +-- documentation and/or other materials provided with the distribution. +-- * Neither the name of the University of Kent nor the names of its +-- contributors may be used to endorse or promote products derived from +-- this software without specific prior written permission. +-- +-- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +-- IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, +-- THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +-- PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +-- CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +-- EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +-- PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +-- PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +-- LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +-- NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +-- SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + +-- | A module for running items in parallel. See +-- for details of how parallel items are modelled. +-- +-- Parallel specifications are well supported, and the only change to this module +-- from normal CHP is that forking is not currently supported. +module Control.Concurrent.CHPSpec.Parallel (runParallel, runParallel_, (<||>), (<|*|>), + runParMapM, runParMapM_) where + +import Control.Arrow +import Control.Monad.Reader + +import Control.Concurrent.CHPSpec.Base +import Control.Concurrent.CHPSpec.Spec + +runParallel :: [CHP a] -> CHP [a] +runParallel = addSpecT1 . liftM (second Par . unzip) . mapM finSpecT + +runParMapM :: (a -> CHP b) -> [a] -> CHP [b] +runParMapM f = runParallel . map f + +runParMapM_ :: (a -> CHP b) -> [a] -> CHP () +runParMapM_ f = runParallel_ . map f + +(<||>) :: CHP a -> CHP b -> CHP (a, b) +(<||>) p q = do [x, y] <- runParallel [liftM Left p, liftM Right q] + combine x y + where + combine :: Monad m => Either a b -> Either a b -> m (a, b) + combine (Left x) (Right y) = return (x, y) + combine (Right y) (Left x) = return (x, y) + -- An extra case to keep the compiler happy: + combine _ _ = error "Impossible combination values in <|^|>" + +(<|*|>) :: CHP a -> CHP b -> CHP () +(<|*|>) p q = runParallel_ [p >> return (), q >> return ()] + +runParallel_ :: [CHP a] -> CHP () +runParallel_ procs = runParallel procs >> return () + +-- We right associate to allow the liftM fst ((readResult) <||> runParallel_ +-- workers) pattern +infixr <||> +-- Doesn't really matter for this operator: +infixr <|*|> + diff --git a/Control/Concurrent/CHPSpec/Print.hs b/Control/Concurrent/CHPSpec/Print.hs new file mode 100644 --- /dev/null +++ b/Control/Concurrent/CHPSpec/Print.hs @@ -0,0 +1,90 @@ +module Control.Concurrent.CHPSpec.Print where + +import Control.Applicative +import Control.Arrow +import Control.Compose (Flip(..)) +import qualified Data.Foldable as F +import Data.List (intersperse) +import qualified Data.Map as Map +import Data.Maybe +import qualified Data.Set as Set +import qualified Data.Traversable as T +import qualified Text.PrettyPrint.HughesPJ as PP + +import Control.Concurrent.CHPSpec.Spec + +name :: String -> PP.Doc +name s = PP.text [if c `elem` valid then c else '_' | c <- s] + where + valid = ['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9'] ++ "?!." + +pprintForwardDecl :: String -> PP.Doc +pprintForwardDecl n = PP.sep [PP.text "channel", name $ eventName n] + +type ProcEvents = Map.Map String (Set.Set String) + +pprintProc :: ProcEvents -> (String, Spec' String String) -> PP.Doc +pprintProc m (n, spec) + = PP.hang (PP.hcat [name n, PP.text "="]) + 2 (pprintCSP_Seq m spec) + +pprintCSP_Seq :: ProcEvents -> Spec' String String -> PP.Doc +pprintCSP_Seq m = PP.parens . PP.sep . p + where + p [] = [PP.text "SKIP"] + p (Sync c : xs) = [name c, PP.text "->"] ++ p xs + p [x] = [pprintCSP m x] + p (x:xs) = [pprintCSP m x, PP.text ";"] ++ p xs + +pprintCSP :: ProcEvents -> SpecItem' String String -> PP.Doc +pprintCSP m (Alt s) = zeroOneMore m "STOP" (withOp m "[]") s +pprintCSP m (Par xs) = zeroOneMore m "SKIP" joinPar xs + where + joinPar :: [Spec' String String] -> PP.Doc + joinPar [a] = pprintCSP_Seq m a + joinPar (a:bs) = PP.parens $ PP.sep $ + [ pprintCSP_Seq m a + , pprintParOp (findAllComms eventName m a `Set.intersection` + unionAll (map (findAllComms eventName m) bs)) + , joinPar bs + ] + joinPar _ = error "Impossible code reached in pprintCSP" +pprintCSP _ (Call p) = name p +pprintCSP _ x = error $ "pprintCSP: " ++ show x + +withOp :: ProcEvents -> String -> [Spec' String String] -> PP.Doc +withOp m s = PP.parens . PP.sep . intersperse (PP.text s) . map (pprintCSP_Seq m) + +zeroOneMore :: ProcEvents -> String -> + ([Spec' String String] -> PP.Doc) -> [Spec' String String] -> PP.Doc +zeroOneMore _ zeroText _ [] = PP.text zeroText +zeroOneMore m _ _ [x] = pprintCSP_Seq m x +zeroOneMore _ _ f xs = f xs + +eventName :: String -> String +eventName = takeWhile (`notElem` "?!.") + +pprintParOp :: Set.Set String -> PP.Doc +pprintParOp s + | Set.null s = PP.text "|||" + | otherwise = surround "[|{|" "|}|]" $ intersperse PP.comma $ map name (Set.toList s) + where + surround a b x = PP.sep $ [PP.text a] ++ x ++ [PP.text b] + +findAllComms :: forall f p c c'. (Show p, Ord p, Ord c', Functor f, F.Foldable f) => + (c -> c') -> Map.Map p (Set.Set c') -> f (SpecItem' p c) -> Set.Set c' +findAllComms f m = uncurry Set.union . (actualComms &&& lookupComms) + where + actualComms, lookupComms :: f (SpecItem' p c) -> Set.Set c' + actualComms = unionAll . fmap (unionAll . fmap (Set.singleton . f)) + lookupComms = unionAll . fmap (unionAll . fmap (\n -> fromMaybe (error $ "findAllComms " ++ show (n, Map.keys m)) $ Map.lookup n m) . Flip) + +unionAll :: (F.Foldable f, Ord a) => f (Set.Set a) -> Set.Set a +unionAll = F.foldr Set.union Set.empty + + +pullUpRepeatM :: (Functor m, Monad m) => (Spec' proc comm -> m proc) -> SpecItem' proc comm -> m (SpecItem' proc comm) +pullUpRepeatM f (Par xs) = Par <$> T.mapM (T.mapM $ pullUpRepeatM f) xs +pullUpRepeatM f (Alt xs) = Alt <$> T.mapM (T.mapM $ pullUpRepeatM f) xs +pullUpRepeatM f (Repeat x) = Call <$> f x +pullUpRepeatM _ x = return x diff --git a/Control/Concurrent/CHPSpec/Process.hs b/Control/Concurrent/CHPSpec/Process.hs new file mode 100644 --- /dev/null +++ b/Control/Concurrent/CHPSpec/Process.hs @@ -0,0 +1,111 @@ +-- Communicating Haskell Processes. +-- Copyright (c) 2009-2010, Neil Brown. +-- All rights reserved. +-- +-- Redistribution and use in source and binary forms, with or without +-- modification, are permitted provided that the following conditions are +-- met: +-- +-- * Redistributions of source code must retain the above copyright +-- notice, this list of conditions and the following disclaimer. +-- * Redistributions in binary form must reproduce the above copyright +-- notice, this list of conditions and the following disclaimer in the +-- documentation and/or other materials provided with the distribution. +-- * Neither the name of the Neil Brown nor the names of other +-- contributors may be used to endorse or promote products derived from +-- this software without specific prior written permission. +-- +-- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +-- IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, +-- THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +-- PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +-- CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +-- EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +-- PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +-- PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +-- LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +-- NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +-- SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + +-- | A module providing the process annotation for recursive processes. +module Control.Concurrent.CHPSpec.Process (Process, process, subProcess) where + +import Control.Applicative +import Control.Monad.State +import Data.Dynamic (Dynamic, fromDyn, fromDynamic, toDyn) +import qualified Data.List as L +import Data.Typeable (Typeable) +import qualified Data.Map as Map + +import Control.Concurrent.CHPSpec.Base +import Control.Concurrent.CHPSpec.Spec + +checkArgs :: [Dynamic] -> [Dynamic -> Bool] -> Bool +checkArgs ds fs + | length ds /= length fs = False + | otherwise = and $ zipWith ($) fs ds + +-- | A class with instances for CHP processes of the form @a -> b -> .. -> CHP r@. +-- +-- The return value of the process must support 'Typeable', and the arguments of +-- the process must support 'Typeable' and 'Eq'. +class Process p where + -- Internal use only: + process' :: Bool -> String -> [(Dynamic, CheckArg)] -> p -> p + +instance (Typeable a) => Process (CHP a) where + process' topLevel name immArgs p = addSpecT1 $ do + st <- get + let possibles = Map.toList <$> (Map.lookup name $ chpProcessMap st) + args = if topLevel then immArgs + else chpFreeNames st ++ immArgs + case possibles >>= L.find (checkArgs (map fst args) . fst . snd) of + Just (n, (_, (_, r))) + -> return (flip fromDyn (error "process-lookup") r, Call n) + Nothing -> + do let n = chpNextProcess st + put $ st { chpProcessMap = insertMapMap name n + (map snd args, (error "process", toDyn ())) $ chpProcessMap st + , chpFreeNames = args + , chpNextProcess = succ n + } + (r, f) <- finSpecT p + modify $ \st' -> st' { chpProcessMap = insertMapMap name n + (map snd args, (f, toDyn r)) $ chpProcessMap st' + -- Restore original free names: + , chpFreeNames = chpFreeNames st } + return (r, Call n) + +instance (Eq a, Typeable a, Process b) => Process (a -> b) where + process' topLevel name args f x + = process' topLevel name (args ++ [(toDyn x, (== Just x) . fromDynamic)]) (f x) + +-- | An annotation to put around a top-level process. This annotation must be +-- inside the recursive knot. You can either place it as: +-- +-- > foo :: Int -> String -> CHP () +-- > foo = process "foo" $ \n s -> ... +-- +-- Or as follows: +-- +-- > foo :: Int -> String -> CHP () +-- > foo = process "foo" foo' +-- > where +-- > foo' n s = ... +-- +-- The annotation must capture all the parameters to the process. What you must /not/ do is place it +-- such that there are free parameters not captured, for example this is /wrong/: +-- +-- > foo :: Int -> String -> CHP () +-- > foo n s = process "foo" foo' +-- > where +-- > foo' = ... +-- +-- If you do want to have recursive processes that have outer parameters and not +-- pass them, you must wrap the outer process in 'process' and the inner process(es) +-- in 'subProcess'. +process :: Process p => String -> p -> p +process s = process' True s [] + +subProcess :: Process p => String -> p -> p +subProcess s = process' False s [] diff --git a/Control/Concurrent/CHPSpec/Spec.hs b/Control/Concurrent/CHPSpec/Spec.hs new file mode 100644 --- /dev/null +++ b/Control/Concurrent/CHPSpec/Spec.hs @@ -0,0 +1,140 @@ +-- Communicating Haskell Processes. +-- Copyright (c) 2010, Neil Brown. +-- All rights reserved. +-- +-- Redistribution and use in source and binary forms, with or without +-- modification, are permitted provided that the following conditions are +-- met: +-- +-- * Redistributions of source code must retain the above copyright +-- notice, this list of conditions and the following disclaimer. +-- * Redistributions in binary form must reproduce the above copyright +-- notice, this list of conditions and the following disclaimer in the +-- documentation and/or other materials provided with the distribution. +-- * Neither the name of Neil Brown nor the names of other +-- contributors may be used to endorse or promote products derived from +-- this software without specific prior written permission. +-- +-- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +-- IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, +-- THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +-- PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +-- CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +-- EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +-- PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +-- PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +-- LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +-- NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +-- SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +module Control.Concurrent.CHPSpec.Spec where + +import Control.Compose (Flip(..)) +import qualified Data.Foldable as F +import Data.List (nub) + +-- Specification: +data SpecItem' proc comm + = Par [Spec' proc comm] + | Alt [Spec' proc comm] + | Call proc + | Sync comm + | Stop + | Repeat (Spec' proc comm) + deriving (Show) + +type Spec' proc comm = [SpecItem' proc comm] + +data Dir = DirInput | DirOutput deriving (Eq, Read, Show) + +type ProcessId = Integer + +type EventId = Integer + +type CommId = Either EventId (EventId, Dir, Integer) + +type SpecItem = SpecItem' ProcessId CommId + +type Spec = Spec' ProcessId CommId + +type SpecMod = Spec -> Spec + +finalise :: SpecMod -> Spec +finalise f = f [] + +-- Instances: + +instance Functor (SpecItem' p) where + fmap _ (Call x) = Call x + fmap f (Sync x) = Sync $ f x + fmap _ Stop = Stop + fmap f (Repeat x) = Repeat $ fmap (fmap f) x + fmap f (Alt x) = Alt $ fmap (fmap (fmap f)) x + fmap f (Par x) = Par $ fmap (fmap (fmap f)) x + +instance Functor (Flip SpecItem' c) where + fmap f = Flip . fmap' . unFlip + where + fmap' (Call x) = Call $ f x + fmap' (Sync x) = Sync x + fmap' Stop = Stop + fmap' (Repeat x) = Repeat $ fmap fmap' x + fmap' (Alt x) = Alt $ fmap (fmap fmap') x + fmap' (Par x) = Par $ fmap (fmap fmap') x + +instance F.Foldable (SpecItem' p) where + foldr f x (Par xs) = F.foldr (flip $ F.foldr (flip $ F.foldr f)) x xs + foldr f x (Alt xs) = F.foldr (flip $ F.foldr (flip $ F.foldr f)) x xs + foldr _ x (Call _) = x + foldr _ x Stop = x + foldr f x (Sync y) = f y x + foldr f x (Repeat y) = F.foldr (flip $ F.foldr f) x y + +instance F.Foldable (Flip SpecItem' c) where + foldr = (\f x -> foldr' f x . unFlip) + where + foldr' f x (Par xs) = F.foldr (flip $ F.foldr (flip $ foldr' f)) x xs + foldr' f x (Alt xs) = F.foldr (flip $ F.foldr (flip $ foldr' f)) x xs + foldr' f x (Call y) = f y x + foldr' _ x (Sync _) = x + foldr' _ x Stop = x + foldr' f x (Repeat y) = F.foldr (flip $ foldr' f) x y + +instance (Eq a, Eq b) => Eq (SpecItem' a b) where + (==) (Call x) (Call y) = x == y + (==) (Sync x) (Sync y) = x == y + (==) (Repeat x) (Repeat y) = x == y + (==) (Par x) (Par y) = bagsEqual x y + (==) (Alt x) (Alt y) = x == y + (==) Stop Stop = True + (==) _ _ = False + +bagsEqual :: Eq a => [a] -> [a] -> Bool +bagsEqual [] [] = True +bagsEqual _ [] = False +bagsEqual [] _ = False +bagsEqual (x:xs) ys + | 1 + length xs /= length ys = False + | otherwise + = case span (/= x) ys of + (_, []) -> False + (as, _:bs) -> bagsEqual xs (as ++ bs) + +checkZipWith :: (a -> b -> c) -> [a] -> [b] -> [c] +checkZipWith f xs ys + | length xs /= length ys = error "checkZipWith, wrong lengths" + | otherwise = zipWith f xs ys + +-- Removes single-item Pars, and removes duplicate Alt branches: +pruneSpec :: (Eq p, Eq c) => Spec' p c -> Spec' p c +pruneSpec = concatMap pruneSpecOne + where + pruneSpecOne :: (Eq p, Eq c) => SpecItem' p c -> Spec' p c + pruneSpecOne (Par [x]) = pruneSpec x + pruneSpecOne (Par xs) = [Par $ map pruneSpec xs] + pruneSpecOne (Alt xs) = [Alt $ nub $ map pruneSpec xs] + pruneSpecOne (Repeat x) = [Repeat $ pruneSpec x] + pruneSpecOne x = [x] + +-- First map is process names, second map is channel names +subSpec :: (p -> p') -> (c -> c') -> SpecItem' p c -> SpecItem' p' c' +subSpec fp fc = unFlip . fmap fp . Flip . fmap fc diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,27 @@ +Copyright (c) 2008, University of Kent. +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are +met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + * Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in the + documentation and/or other materials provided with the distribution. + * Neither the name of the University of Kent nor the names of its + contributors may be used to endorse or promote products derived from + this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, +THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/Setup.lhs b/Setup.lhs new file mode 100644 --- /dev/null +++ b/Setup.lhs @@ -0,0 +1,5 @@ +#! /usr/bin/env runhaskell + +> import Distribution.Simple +> main = defaultMain + diff --git a/chp-spec.cabal b/chp-spec.cabal new file mode 100644 --- /dev/null +++ b/chp-spec.cabal @@ -0,0 +1,45 @@ +Name: chp-spec +Version: 1.0.0 +Synopsis: A mirror implementation of chp that generates a specification of the program +License: BSD3 +License-file: LICENSE +Author: Neil Brown +Maintainer: neil@twistedsquare.com +Copyright: Copyright (c) 2009--2010, University of Kent +Stability: Stable +Tested-with: GHC==6.10.4, GHC==6.12.1 +Description: This library mirrors the API of much of the CHP library, but + instead of executing the program properly, using this library + will generate the CSP specification of your program. See + this article for details and caveats: +Homepage: http://www.cs.kent.ac.uk/projects/ofa/chp/ +Category: Concurrency + +Cabal-Version: >= 1.2.3 +Build-Type: Simple +Build-Depends: base >= 4 && < 5, containers, deepseq >= 1.1 && < 1.2, mtl, pretty, TypeCompose >= 0.7 && < 0.8 + +Exposed-modules: Control.Concurrent.CHPSpec + Control.Concurrent.CHPSpec.Alt + Control.Concurrent.CHPSpec.Barriers + Control.Concurrent.CHPSpec.Channels + Control.Concurrent.CHPSpec.Channels.Communication + Control.Concurrent.CHPSpec.Channels.Creation + Control.Concurrent.CHPSpec.Channels.Ends + Control.Concurrent.CHPSpec.Channels.Synonyms + Control.Concurrent.CHPSpec.Enroll + Control.Concurrent.CHPSpec.LazySmallCheck + Control.Concurrent.CHPSpec.Monad + Control.Concurrent.CHPSpec.Parallel + +Other-modules: Control.Concurrent.CHPSpec.Base + Control.Concurrent.CHPSpec.CSP + Control.Concurrent.CHPSpec.Channels.Base + Control.Concurrent.CHPSpec.Process + Control.Concurrent.CHPSpec.Print + Control.Concurrent.CHPSpec.Spec + +Extensions: BangPatterns DeriveDataTypeable FlexibleContexts FlexibleInstances + MultiParamTypeClasses Rank2Types ScopedTypeVariables TypeSynonymInstances + +GHC-Options: -Wall -auto-all