packages feed

chp-spec (empty) → 1.0.0

raw patch · 21 files changed

+1842/−0 lines, 21 filesdep +TypeComposedep +basedep +containerssetup-changed

Dependencies added: TypeCompose, base, containers, deepseq, mtl, pretty

Files

+ Control/Concurrent/CHPSpec.hs view
@@ -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++++
+ Control/Concurrent/CHPSpec/Alt.hs view
@@ -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 <http://chplib.wordpress.com/2010/04/20/automatic-model-generation-part-3-choice-and-io/>+-- 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 <->+
+ Control/Concurrent/CHPSpec/Barriers.hs view
@@ -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+
+ Control/Concurrent/CHPSpec/Base.hs view
@@ -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
+ Control/Concurrent/CHPSpec/CSP.hs view
@@ -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)
+ Control/Concurrent/CHPSpec/Channels.hs view
@@ -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 <http://chplib.wordpress.com/2010/04/22/automatic-model-generation-part-4-communication/>+-- 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
+ Control/Concurrent/CHPSpec/Channels/Base.hs view
@@ -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+
+ Control/Concurrent/CHPSpec/Channels/Communication.hs view
@@ -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
+ Control/Concurrent/CHPSpec/Channels/Creation.hs view
@@ -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)
+ Control/Concurrent/CHPSpec/Channels/Ends.hs view
@@ -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
+ Control/Concurrent/CHPSpec/Channels/Synonyms.hs view
@@ -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'
+ Control/Concurrent/CHPSpec/Enroll.hs view
@@ -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_
+ Control/Concurrent/CHPSpec/LazySmallCheck.hs view
@@ -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: <http://chplib.wordpress.com/2010/04/20/automatic-model-generation-part-3-choice-and-io/>+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+
+ Control/Concurrent/CHPSpec/Monad.hs view
@@ -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: <http://chplib.wordpress.com/2010/04/20/automatic-model-generation-part-3-choice-and-io/>+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' ""
+ Control/Concurrent/CHPSpec/Parallel.hs view
@@ -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 <http://chplib.wordpress.com/2010/04/13/automatic-model-generation-part-1-parallel/>+-- 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 <|*|>+
+ Control/Concurrent/CHPSpec/Print.hs view
@@ -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
+ Control/Concurrent/CHPSpec/Process.hs view
@@ -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 []
+ Control/Concurrent/CHPSpec/Spec.hs view
@@ -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
+ LICENSE view
@@ -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.
+ Setup.lhs view
@@ -0,0 +1,5 @@+#! /usr/bin/env runhaskell++> import Distribution.Simple+> main = defaultMain+
+ chp-spec.cabal view
@@ -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: <http://chplib.wordpress.com/2010/05/03/new-chp-spec-library-released/>+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