CSPM-FiringRules-0.4.0.0: src/CSPM/FiringRules/Test/Gen.hs
-----------------------------------------------------------------------------
-- |
-- Module : CSPM.CoreLanguage.FiringRules.Gen
-- Copyright : (c) Fontaine 2010
-- License : BSD
--
-- Maintainer : fontaine@cs.uni-duesseldorf.de
-- Stability : experimental
-- Portability : GHC-only
--
-- Generation of arbitrary processes and proof trees for QuickCheck-testing.
--
-----------------------------------------------------------------------------
{-# LANGUAGE FlexibleInstances,TypeSynonymInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
module CSPM.FiringRules.Test.Gen where
import CSPM.CoreLanguage
import CSPM.CoreLanguage.Event
import CSPM.FiringRules.Rules
import Test.QuickCheck.Arbitrary
import Test.QuickCheck.Gen
import Control.Monad
import Control.Applicative
import qualified Data.List as List
class (BL i) => Arb i where
genPrefix :: i -> Event i -> Gen (Prefix i)
arbitraryEvent :: i -> Gen (Event i)
arbitraryEventSet :: i -> Gen (EventSet i)
arbitraryRenaming :: i -> Gen (RenamingRelation i)
arbitraryRenaming ty = liftM (renamingFromList ty) $ arbitraryRenamingDR ty e e
where e = allEvents ty
arbitraryRenamingDR :: i -> EventSet i -> EventSet i -> Gen [(Event i, Event i)]
arbitraryRenamingDR ty domain range
= listOf1 $ liftM2 (,)
(elements $ eventSetToList ty domain)
(elements $ eventSetToList ty range)
mkArb :: Arbitrary a => (a -> t) -> Gen t
mkArb f = fmap f arbitrary
mkArb2 :: (Arbitrary a,Arbitrary b) => (a -> b -> t) -> Gen t
mkArb2 f = liftM2 f arbitrary arbitrary
mkArb3 ::
(Arbitrary a, Arbitrary b, Arbitrary c) =>
(a -> b -> c-> t) -> Gen t
mkArb3 f = liftM3 f arbitrary arbitrary arbitrary
instance Arb i => Arbitrary (Process i) where arbitrary = sized genProcess
arbitraryPrefix :: forall i. Arb i => i -> Gen (Prefix i)
arbitraryPrefix i = do
arbitraryEvent i >>= genPrefix i
genProcess :: forall i. Arb i => Int -> Gen (Process i)
genProcess 0 = elements $ [Stop,Skip,Omega] ++ atomicProcesses
where atomicProcesses = map AProcess [1..5]
genProcess n = frequency [
(10, liftM Prefix $ arbitraryPrefix ty)
,(10, binProc ExternalChoice)
,(10, binProc InternalChoice)
,(10, binProc Interleave)
,(10, binProc Interrupt)
,(10, liftM3 Sharing subProcess (arbitraryEventSet ty) subProcess)
,(10, binProc Seq)
,(10, liftM2 Hide (arbitraryEventSet ty) arbitrary)
,(30, genProcess 0)
,(10, liftM3 Exception (arbitraryEventSet ty) subProcess subProcess)
]
where
binProc c = liftM2 c subProcess subProcess
subProcess = resize (n `div` 2) arbitrary
ty = (undefined :: i)
instance Arb i => Arbitrary (RuleEvent i) where arbitrary = arbitraryRE
arbitraryRE :: forall i. Arb i => Gen (RuleEvent i)
arbitraryRE = sized $ \size -> do
arbitraryEvent (undefined :: i) >>= genRule size
instance Arb i => Arbitrary (RuleTau i) where
arbitrary = sized genRuleTau
genRuleTau :: forall i. Arb i => Int -> Gen (RuleTau i)
genRuleTau 0 = oneof [ mkArb2 InternalChoiceL, mkArb2 InternalChoiceR ]
genRuleTau n = frequency [
f10 $ do
h <- arbSet
hiddenEvent <- elements $ (eventSetToList ty) (allEvents ty)
r <- genRule n hiddenEvent
return $ Hidden (insert ty hiddenEvent h) r
,f10 $ ExtChoiceTauL <$> subRule <*> p
,f10 $ ExtChoiceTauR <$> p <*> subRule
,f10 $ SeqTick <$> subRuleTick <*> p
,f10 $ SeqTau <$> subRule <*> p
,f10 $ ShareTauL <$> arbSet <*> subRule <*> p
,f10 $ ShareTauR <$> arbSet <*> p <*> subRule
,f10 $ ShareTickL <$> arbSet <*> subRuleTick <*> p
,f10 $ ShareTickR <$> arbSet <*> p <*> subRuleTick
,f10 $ AParallelTauL <$> arbSet <*> arbSet <*> subRule <*> p
,f10 $ AParallelTauR <$> arbSet <*> arbSet <*> p <*> subRule
,f10 $ AParallelTickL <$> arbSet <*> arbSet <*> subRuleTick <*> p
,f10 $ AParallelTickR <$> arbSet <*> arbSet <*> p <*> subRuleTick
,f10 $ InterleaveTauL <$> subRule <*> p
,f10 $ InterleaveTauR <$> p <*> subRule
,f10 $ InterleaveTickL <$> subRuleTick <*> p
,f10 $ InterleaveTickR <$> p <*> subRuleTick
,f10 $ InterruptTauL <$> subRule <*> p
,f10 $ InterruptTauR <$> p <*> subRule
,f10 $ TimeoutTauR <$> subRule <*> p
,f10 $ TimeoutOccurs <$> p <*> p
,f10 $ ChaosStop <$> arbSet
,f10 $ LinkTauL <$> arbitraryRenaming ty <*> subRule <*> p
,f10 $ LinkTauR <$> arbitraryRenaming ty <*> p <*> subRule
,f10 $ LinkTickL <$> arbitraryRenaming ty <*> subRuleTick <*> p
,f10 $ LinkTickR <$> arbitraryRenaming ty <*> p <*> subRuleTick
,f10 $ do
rel <- arbitraryRenaming ty
(e1,e2) <- elements (renamingToList ty rel)
LinkLinked rel <$> subRuleEvent e1 <*> subRuleEvent e2
]
where
subRule :: Gen (RuleTau i)
subRule = genRuleTau $ n `div` 2
subRuleTick :: Gen (RuleTick i)
subRuleTick = genRuleTick $ n `div` 2
subRuleEvent :: Event i -> Gen (RuleEvent i)
subRuleEvent e = genRule (n `div` 2) e
ty = (undefined :: i)
p :: Gen (Process i)
p = arbitrary
f10 x = (10,x)
arbSet = arbitraryEventSet ty
instance Arb i => Arbitrary (RuleTick i) where
arbitrary = sized genRuleTick
genRuleTick :: forall i. Arb i => Int -> Gen (RuleTick i)
genRuleTick 0 = oneof
[ liftM ShareOmega $ arbitraryEventSet (undefined :: i)
, return InterleaveOmega ]
genRuleTick n = frequency [
f10 $ return SkipTick
,f10 $ HiddenTick <$> arbSet <*> r
,f10 $ ShareOmega <$> arbSet
,f10 $ return InterleaveOmega
,f10 $ ExtChoiceTickL <$> r <*> p
,f10 $ ExtChoiceTickR <$> p <*> r
,f10 $ InterruptTick <$> r <*> p
,f10 $ TimeoutTick <$> r <*> p
,f10 $ RenamingTick <$> arbitraryRenaming ty <*> r
,f10 $ LinkParallelTick <$> arbitraryRenaming ty
,f10 $ AParallelOmega <$> arbSet <*> arbSet
,f10 $ RepAParallelOmega <$> (resize 4 $ listOf1 arbSet)
]
where
r :: Gen (RuleTick i)
r = genRuleTick $ n `div` 2
p :: Gen (Process i)
p = arbitrary
f10 x = (10,x)
arbSet = arbitraryEventSet ty
ty = (undefined :: i)
genRule :: forall i. Arb i => Int -> Event i -> Gen (RuleEvent i)
genRule 0 event = HPrefix event <$> genPrefix (undefined :: i) event
genRule n event = frequency [
f10 $ ExtChoiceL <$> r <*> p
,f10 $ ExtChoiceR <$> p <*> r
,f10 $ InterleaveL <$> r <*> p
,f10 $ InterleaveR <$> p <*> r
,f10 $ SeqNormal <$> r <*> p
,f10 $ NotHidden <$> setWithoutEvent <*> genRule n event
,f10 $ NotShareL <$> setWithoutEvent <*> r <*> p
,f10 $ NotShareR <$> setWithoutEvent <*> p <*> r
,f10 $ Shared <$> setWithEvent <*> r <*> r
,f10 $ ChaosEvent <$> setWithEvent <*> pure event
,f10 $ AParallelL <$> setWithEvent <*> setWithoutEvent <*> r <*> p
,f10 $ AParallelR <$> setWithoutEvent <*> setWithEvent <*> p <*> r
,f10 $ AParallelBoth <$> setWithEvent <*> setWithEvent <*> r <*> r
,f10 $ arbitraryRepAParallelEvent
,f10 $ NoInterrupt <$> r <*> p
,f10 $ InterruptOccurs <$> p <*> r
,f10 $ TimeoutNo <$> r <*> p
,f10 $ do
t <- arbitraryRenamingDR ty (allEvents ty) (allEvents ty)
newEvent <- arbitraryEvent ty
let rel = renamingFromList ty ((newEvent, event) : t)
Rename rel event <$> genRule (n `div` 2) newEvent
,f10 $ do
rel <- arbitraryRenamingDR ty
(delete ty event (allEvents ty))
(allEvents ty)
RenameNotInDomain (renamingFromList ty rel) <$> r
,(30, genRule 0 event)
,f10 $ do
rel <- arbitraryRenamingDR ty
(delete ty event (allEvents ty))
(allEvents ty)
LinkEventL (renamingFromList ty rel) <$> r <*> p
,f10 $ do
rel <- arbitraryRenamingDR ty
(allEvents ty)
(delete ty event (allEvents ty))
LinkEventR (renamingFromList ty rel) <$> p <*> r
,f10 $ NoException <$> setWithoutEvent <*> r <*> p
,f10 $ ExceptionOccurs <$> setWithEvent <*> p <*> r
]
where
p :: Gen (Process i)
p = arbitrary
r :: Gen (RuleEvent i)
r = genRule (n `div` 2) event
f10 x = (10,x)
arbSet = arbitraryEventSet ty
setWithEvent :: Gen (EventSet i)
setWithEvent = do
x <- arbSet
return $ insert ty event x
setWithoutEvent :: Gen (EventSet i)
setWithoutEvent = do
x <- arbSet
return $ delete ty event x
ty = (undefined :: i)
arbitraryRepAParallelEvent :: Gen (RuleEvent i)
arbitraryRepAParallelEvent = do
flags <- (resize 4 $ listOf1 arbitrary) -- hardcoded max 4 processes
`suchThat` List.or
RepAParallelEvent <$> mapM repAPart flags
repAPart :: Bool -> Gen (EventRepAPart i)
repAPart True = Right <$> liftM2 (,) setWithEvent r
repAPart False = Left <$> liftM2 (,) setWithoutEvent p