text:
<!DOCTYPE html>

  <title>jQuery Methods</title>
  <link rel="stylesheet" type="text/css" href="lecture156.css">

jQuery Methods: click()

jQuery Methods: keypress()

jQuery Methods: on()

<input type="text" id="keyPresser">

click() <button>click ()</button>

keypress()

on()

<button id="submit">Submit</button>

Please don't fade me

I'm begging you, please

Help, help help!!

<button id="fader">Fader</button>

redpajama_set_name: RedPajamaGithub


text:
{- *** MOCS-COPYRIGHT-NOTICE-BEGIN ***
 -
 - This copyright notice is auto-generated by ./add-copyright-notice.
 - Additional copyright notices must be added below the last line of this notice.
 -
 - MoCS (https://lewis.cs.uni-saarland.de/tools/mocs/): "haskell-frontend/Temporal.hs".
 - The content of this file is copyright of Saarland University -
 - Copyright (C) 2009 Saarland University, Reactive Systems Group, Lars Kuhtz.
 -
 - This file is part of MoCS (https://lewis.cs.uni-saarland.de/tools/mocs/).
 -
 - License: three-clause BSD style license.
 - The license text can be found in the file LICENSE.
 -
 - *** MOCS-COPYRIGHT-NOTICE-END *** -}

{-# LANGUAGE FlexibleContexts #-}
{- Logic:
 - * Prop
 - * WeakReg    (weak)
 - * StrongReg  (strong)
 -
 - * Negate
 - * And
 - * Or
 -
 - * Next     (weak)
 - * BNext     (weak)
 - * WNext    (strong)
 - * WBNext    (strong)
 -
 - * Until    (strong)  (sugar)
 - * Waitfor  (weak)    (sugar)
 - * BUntil   (strong)
 - * BWaitfor (weak)
 -
 - * Release   (weak)    (sugar)
 - * SRelease  (strong)  (sugar)
 - * BRelease  (weak)
 - * SBRelease (strong)
 -
 - * Globally   (weak)    (sugar)
 - * BGlobally  (weak)
 - * SBGlobally (strong)
 -
 - * Eventually   (strong) (sugar)
 - * BEventually  (strong)
 - * WBEventually (weak)
 -
 - * Abort
 - * Simplies
 -}

module Temporal
  ( Formula(..)
  , mkProp
  , mkWeakReg
  , mkStrongReg

  , mkNegate
  , mkAnd
  , mkOr

  , mkNext
  , mkBNext
  , mkWNext
  , mkWBNext

  , mkUntil
  , mkWaitfor
  , mkBUntil
  , mkBWaitfor

  , mkRelease
  , mkSRelease
  , mkBRelease
  , mkSBRelease

  , mkGlobally
  , mkBGlobally
  , mkSBGlobally

  , mkEventually
  , mkBEventually
  , mkWBEventually

  , mkAbort
  , mkSImplies

  , mkImplies
  , mkEquiv

  , formula
  , parser
  , pushNegations
  , simplify
  --, unfoldLevelF
  --, unfoldF
  --, unfoldAllF
  --, unfoldBoundedF
  , pushNextRec
  , allSubf
  , allLeaves
  , dual
  , rec
  , toString
  , allRegProps
  , allRegs
  , allProps
  , isBounded
  )

where

import qualified Text.ParserCombinators.Parsec as P
import Text.ParserCombinators.Parsec.Expr

import Data.Typeable
import Data.List

import PSLLexer
import ToString
import PSLFragment
import Ordinal

-- usualy reg should be defined upon prop as well.
data Formula reg prop
  = Prop prop
  | WeakReg (reg prop)
  | StrongReg (reg prop)

  | Negate (Formula reg prop)
  | And (Formula reg prop) (Formula reg prop)
  | Or (Formula reg prop) (Formula reg prop)

  | Next Bound (Formula reg prop)
  | WNext Bound (Formula reg prop)

  | Until Bound (Formula reg prop) (Formula reg prop)
  | Waitfor Bound (Formula reg prop) (Formula reg prop)
  | Release Bound (Formula reg prop) (Formula reg prop)
  | SRelease Bound (Formula reg prop) (Formula reg prop)

  | Globally Bound (Formula reg prop)
  | SGlobally Bound (Formula reg prop)
  | Eventually Bound (Formula reg prop)
  | WEventually Bound (Formula reg prop)

  | Abort (Formula reg prop) prop
  | SImplies (reg prop) (Formula reg prop)
  deriving (Eq, Ord,Show)

instance (Typeable (reg prop), Typeable prop) => Typeable (Formula reg prop) where
  typeOf f = mkTyConApp (mkTyCon "Formula") [typeOf f]

instance (PSLFragment (reg prop), PSLFragment prop) => PSLFragment (Formula reg prop) where
  horizon = horizon'
  dual = dual'
  subfmap = rec
  subf = subf'
  parser = formula
  constant = mkProp . constant
  simplify = simplify'
  constr = constr'

-- horizon
horizon' (Prop p) = horizon p
horizon' (WeakReg r) = horizon r
horizon' (StrongReg r) = horizon r

horizon' (Negate f) = horizon' f
horizon' (And f g) = max (horizon' f) (horizon' g)
horizon' (Or f g) = max (horizon' f) (horizon' g)

horizon' (Next b f) = horizon' f + b
horizon' (WNext b f) = horizon' f + b

horizon' (Until b f g) = max (b + horizon' f) ((b - 1) + horizon' g)
horizon' (Waitfor b f g) = max (b + horizon' f) ((b - 1) + horizon' g)
horizon' (Release b f g) = max (b + horizon' f) (b + horizon' g)
horizon' (SRelease b f g) = max (b + horizon' f) (b + horizon' g)

horizon' (Globally b f) = horizon' f + b
horizon' (SGlobally b f) = horizon' f + b
horizon' (Eventually b f) = horizon' f + b
horizon' (WEventually b f) = horizon' f + b

horizon' (Abort f _) = horizon' f
horizon' (SImplies r f) = (horizon r) + (horizon' f) - 1

-- generator
mkProp e = Prop e
mkWeakReg s = WeakReg s
mkStrongReg b = StrongReg b

mkNegate x = Negate x
mkAnd x y | x < y =  And x y
          | otherwise = And y x
mkOr x y  | x < y = Or x y
          | otherwise = Or y x

mkNext x = Next 1 x
mkWNext x = WNext 1 x

mkBNext b x = Next b x
mkWBNext b x = WNext b x

mkUntil x y = Until Infty x y
mkWaitfor x y = Waitfor Infty x y
mkBUntil b x y = Until b x y
mkBWaitfor b x y = Waitfor b x y

mkRelease x y = Release Infty x y
mkSRelease x y = SRelease Infty x y
mkBRelease b x y = Release b x y
mkSBRelease b x y = SRelease b x y

mkGlobally x = Globally Infty x
mkBGlobally b x = Globally b x
mkSBGlobally b x = SGlobally b x

mkEventually x = Eventually Infty x
mkBEventually b x = Eventually b x
mkWBEventually b x = WEventually b x

mkAbort f e = Abort f e
mkSImplies r f = SImplies r f

-- suguar
mkImplies x y = mkOr (mkNegate x) y
mkEquiv x y = mkAnd (mkImplies x y) (mkImplies y x)

-------------------------------------------------------------------------------
-- Note: we maintain arguments of associative operators (and, or) ordered.
-- Alternatively we could have coded this into the instanciation of EQ.
-- The ordered approach is probably more efficient. It Requires, however, that
-- The mk-Constructors are always used to create new Formulas.

-------------------------------------------------------------------------------
-- constr
constr' f = case f of
    (Prop _) -> const f
    (StrongReg _) -> const f
    (WeakReg _) -> const f
    (Negate _) -> un mkNegate
    (And _ _) -> bin mkAnd
    (Or _ _) -> bin mkOr
    (Next b _) -> bun mkBNext b
    (WNext b _) -> bun mkWBNext b
    (Until b _ _) -> bbin mkBUntil b
    (Waitfor b _ _) -> bbin mkBWaitfor b
    (Release b _ _) -> bbin mkBRelease b
    (SRelease b _ _) -> bbin mkSBRelease b
    (Globally b _) -> bun mkBGlobally b
    (SGlobally b _) -> bun mkSBGlobally b
    (Eventually b _) -> bun mkBEventually b
    (WEventually b _) -> bun mkWBEventually b
    (Abort _ e) -> (\(x:_) -> mkAbort x e)
    (SImplies r _) -> (\(x:_) -> mkSImplies r x)
    where
    un c = \(x:_) -> c x
    bun c b = \(x:_) -> c b x
    bin c = \(l:r:_) -> c l r
    bbin c b = \(l:r:_) -> c b l r

-------------------------------------------------------------------------------
-- show
-- Currently prints out format used by parser
-- TODO set parenthesis only where needed
instance (Show prop, Show (reg prop), ToString (reg prop), ToString prop) => ToString (Formula reg prop) where
  toString f = case f of
    (Prop e) -> toString e
    (StrongReg r) -> un "\\strong" r
    (WeakReg r) -> toString r

    (Negate f) -> un "\\not" f
    (And f g) -> bin "\\and" f g
    (Or f g) -> bin "\\or" f g

    (Next Infty f) -> un "\\N" f
    (WNext Infty f) -> un "\\wN" f
    (Next b f) -> bbin "\\BN" b f
    (WNext b f) -> bbin "\\wBN" b f

    (Until Infty f g) -> bin "\\U" f g
    (Waitfor Infty f g) -> bin "\\W" f g
    (Until b f g) -> tri "\\BU" b f g
    (Waitfor b f g) -> tri "\\BW" b f g

    (Release Infty f g) -> bin "\\R" f g
    (SRelease Infty f g) -> bin "\\sR" f g
    (Release b f g) -> tri "\\BR" b f g
    (SRelease b f g) -> tri "\\sBR" b f g

    (Globally Infty f) -> un "\\G" f
    (Globally b f) -> bbin "\\BG" b f
    (SGlobally b f) -> bbin "\\sBG" b f

    (Eventually Infty f) -> un "\\F" f
    (Eventually b f) -> bbin "\\BF" b f
    (WEventually b f) -> bbin "\\wBF" b f

    (Abort f e) -> bin "\\abort" f e
    (SImplies r f) -> bin "\\simplies" r f

    where
    un o f = o ++ " " ++ toString f
    bin o f g = "(" ++ toString f ++ " " ++ o ++ " " ++ toString g ++ ")"
    bbin o b f = o ++ " " ++ p b ++ " " ++ toString f
    tri o b f g = "(" ++ toString f ++ " " ++ o ++ " " ++ p b ++ " " ++ toString g ++ ")"
    p b = toString b

-------------------------------------------------------------------------------
-- usefull for variable substitution

-- subformulas as list
subf' (Negate f) = [f]
subf' (Or f g) = [f, g]
subf' (And f g) = [f, g]

subf' (Next _ f) = [f]
subf' (WNext _ f) = [f]

subf' (Globally _ f) = [f]
subf' (SGlobally _ f) = [f]
subf' (Eventually _ f) = [f]
subf' (WEventually _ f) = [f]

subf' (Until _ f g) = [f, g]
subf' (Waitfor _ f g) = [f, g]
subf' (Release _ f g) = [f, g]
subf' (SRelease _ f g) = [f, g]

subf' (Abort f _) = [f]
subf' (SImplies _ f) = [f]

subf' _ = []

allRegs :: Formula reg prop -> [Formula reg prop]
allRegs h = case h of
  (WeakReg _)   -> return h
  (StrongReg _) -> return h
  _             -> subf' h >>= allRegs

allProps :: Formula reg prop -> [Formula reg prop]
allProps h = case h of
  (Prop _) -> return h
  _        -> subf' h >>= allProps

allRegProps :: Formula reg prop -> [Formula reg prop]
allRegProps h = case h of
  (WeakReg _)   -> return h
  (StrongReg _) -> return h
  (Prop _)      -> return h
  _             -> subf' h >>= allRegProps

-- Usefull for mutual recursive defintions (see e.g. pushNegations)
rec :: (Ord (reg prop), Ord prop, PSLFragment (Formula reg prop)) =>
       (Formula reg prop -> Formula reg prop) -> Formula reg prop -> Formula reg prop
rec a f = if atomic f then f else (constr f) (map a (subf f))

-------------------------------------------------------------------------------
-- Dualities
dual' (Prop f) = mkNegate (mkProp f)
dual' (WeakReg f) = mkNegate (mkWeakReg f)
dual' (StrongReg f) = mkNegate (mkStrongReg f)

dual' (Negate f) = f
dual' (Or f g) = mkAnd (dual f) (dual g)
dual' (And f g) = mkOr (dual f) (dual g)

dual' (Next b f) = mkWBNext b (dual f)
dual' (WNext b f) = mkBNext b (dual f)

dual' (Globally b f) = mkBEventually b (dual f)
dual' (SGlobally b f) = mkWBEventually b (dual f)
dual' (Eventually b f) = mkBGlobally b (dual f)
dual' (WEventually b f) = mkSBGlobally b (dual f)

dual' (Until b f g) = mkBRelease b (dual f) (dual g)
dual' (Waitfor b f g) = mkSBRelease b (dual f) (dual g)
dual' (Release b f g) = mkBUntil b (dual f) (dual g)
dual' (SRelease b f g) = mkBWaitfor b (dual f) (dual g)

dual' (Abort f e) = mkNegate (mkAbort f e)
dual' (SImplies r f) = (mkNegate (StrongReg r)) `mkOr` (r `mkSImplies` (dual f))

-------------------------------------------------------------------------------
-- Push negations to state level

pushNegations (Negate f) = dual f
pushNegations f = rec pushNegations f

-------------------------------------------------------------------------------
-- Push Next-Operators
pushNext h = case h of
  (Next b (Negate f)) -> mkNegate $ mkWBNext b f
  (WNext b (Negate f)) -> mkNegate $ mkBNext b f
  (Next b f) -> rec (mkBNext b) f
  (WNext b f) -> rec (mkWBNext b) f
  _ -> h

pushNextRec h = bottomUpRec p' h
  where
  p' h = case h of { (Next b f) -> topDownRec pushNext (mkBNext b f); _ -> h}

-------------------------------------------------------------------------------
-- misc
isBinary f = length (subf f) == 2

isBounded (Next u _) = isFinite u
isBounded (WNext u _) = isFinite u
isBounded (Globally u _) = isFinite u
isBounded (SGlobally u _) = isFinite u
isBounded (Eventually u _) = isFinite u
isBounded (WEventually u _) = isFinite u
isBounded (Until u _ _) = isFinite u
isBounded (Waitfor u _ _) = isFinite u
isBounded (Release u _ _) = isFinite u
isBounded (SRelease u _ _) = isFinite u
isBounded _ = True

allEq [] = True
allEq [_] = True
allEq (a:b:t) = (a == b) && (allEq (b:t))

-------------------------------------------------------------------------------
-- Simplification rules

simplify' f = bottomUpRec (simple5 . simple4 . simple3 . simple2 . simple1) f

simple1 (Abort f e) = mkAbort f e
simple1 (SImplies r f) = mkSImplies r f
simple1 h = if isBinary h && allEq (subf h) then head (subf h) else h

-- (Constants are not part of PSL any more)
simple2 = id

{-
-- Dualities for binary operators
simple3 (Or f g)          | isDual f g = mkConst True
                          | otherwise = mkOr f g
simple3 (And f g)         | isDual f g =  mkConst False
                          | otherwise = mkAnd f g
simple3 (BUntil b f g)    | isDual f g = mkBUntil b (Const True) g
                          | otherwise = mkBUntil b f g
simple3 (BRelease b f g)  | isDual f g = mkConst True
                          | otherwise = mkBRelease b f g
simple3 (WBUntil b f g)   | isDual f g = mkWBUntil b (Const True) g
                          | otherwise = mkWBUntil b f g
simple3 (WBRelease b f g) | isDual f g = mkConst True
                          | otherwise = mkWBRelease b f g
simple3 f = f
-}
simple3 = id

-- Negation
simple4 (Negate f) = dual f
simple4 f = f

-- temporal nesting with equal subformulas
{-
simple5 x = case x of
  (f `Until` (g `Until` h)) -> if f == h || f == g then (g `mkUntil` h) else x
  ((f `Until` g) `Until` h) -> if f == h then (g `mkUntil` f) else
                               if g == h then (f `mkUntil` g) else x
  (BUntil b0 f (BUntil b1 g h)) -> if f == h || f == g then (BUntil (b0+b1) g h) else x
  (BUntil b0 (BUntil b1 f g) h) -> if f == h then (BUntil b0 g f) else
                                   if g == h then (BUntil b1 f g) else x
  -- TODO weak version
  (f `Release` (g `Release` h)) -> if f == h then (h `mkRelease` g) else
                                   if f == g then (g `mkRelease` h) else x
  ((f `Release` g) `Release` h) -> if f == h || g == h then (f `mkRelease` g) else x
  -- TODO bounded version
  -- TODO weak version
  _ -> x
-}
simple5 = id
--balance (And (And f g) h) =
-- TODO: flatten it into a list (use list-monad), elimiate duplicate subformulas,
-- check for contradictions and rebuild a balanced tree.

-- TODO: add more simplification rules in a more systematic way.

-------------------------------------------------------------------------------
-- Unfold temporal operators

{-
-- unfold top level operator
unfoldF f = unfoldF' unfoldF f

-- unfold f i steps
unfoldLevelF 0 f = f
unfoldLevelF i f = unfoldF' (unfoldLevelF (i-1)) f

-- recursively unfold all operators
unfoldAllF f = bottomUpRec unfoldF f

-- recursively unfold all bounded operators
unfoldBoundedF f = bottomUpRec (\x -> if isBounded x then unfoldF x else x) f

-- Fixpoint characterization
unfoldF' r (BUntil (0,0) f g) = g
unfoldF' r (BUntil (_,0) f g) = error "lower bound must not be greater than upper bound"
unfoldF' r (BUntil (0,u) f g) = g `mkOr` (f `mkAnd` (mkNext (r (mkBUntil (0,u-1) f g))))
unfoldF' r (BUntil (l,u) f g) = mkNext (mkBUntil (l-1,u-1) f g)

unfoldF' r (WBUntil (0,0) f g) = g
unfoldF' r (WBUntil (_,0) f g) = error "lower bound must not be greater than upper bound"
unfoldF' r (WBUntil (0,u) f g) = g `mkOr` (f `mkAnd` (mkWNext (r (mkBUntil (0,u-1) f g))))
unfoldF' r (WBUntil (l,u) f g) = mkWNext (mkWBUntil (l-1,u-1) f g)

unfoldF' r (BRelease (0,0) f g) = g
unfoldF' r (BRelease (_,0) f g) = error "lower bound must not be greater than upper bound"
unfoldF' r (BRelease (0,u) f g) = g `mkAnd` (f `mkOr` (mkNext (r (mkBRelease (0,u-1) f g))))
unfoldF' r (BRelease (l,u) f g) = mkNext (mkBRelease (l-1,u-1) f g)

unfoldF' r (WBRelease (0,0) f g) = g
unfoldF' r (WBRelease (_,0) f g) = error "lower bound must not be greater than upper bound"
unfoldF' r (WBRelease (0,u) f g) = g `mkAnd` (f `mkOr` (mkWNext (r (mkWBRelease (0,u-1) f g))))
unfoldF' r (WBRelease (l,u) f g) = mkWNext (mkWBRelease (l-1,u-1) f g)

-- Causes a blowup in the formula (not in the ciruit!)
unfoldF' r (Abort (BUntil (0,0) f g) e) = ((mkProp e) `mkOr` (g `mkAbort`e))
unfoldF' r (Abort (BUntil (_,0) f g) e) = error "lower bound must not be greater than upper bound"
unfoldF' r (Abort (BUntil (0,u) f g) e) = ((mkProp e) `mkOr` ((g `mkAbort`e) `mkOr` ((f `mkAbort`e) `mkAnd` (mkNext (r ((mkBUntil (0,u-1) f g) `mkAbort` e))))))
unfoldF' r (Abort (BUntil (l,u) f g) e) = ((mkProp e) `mkOr` mkNext (mkAbort (mkBUntil (l-1,u-1) f g) e))

unfoldF' r (Abort (WBUntil (0,0) f g) e) = ((mkProp e) `mkOr` (g `mkAbort`e))
unfoldF' r (Abort (WBUntil (_,0) f g) e) = error "lower bound must not be greater than upper bound"
unfoldF' r (Abort (WBUntil (0,u) f g) e) = ((mkProp e) `mkOr` ((g `mkAbort`e) `mkOr` ((f `mkAbort`e) `mkAnd` (mkWNext (r ((mkBUntil (0,u-1) f g) `mkAbort` e))))))
unfoldF' r (Abort (WBUntil (l,u) f g) e) = ((mkProp e) `mkOr` mkWNext (mkAbort (mkWBUntil (l-1,u-1) f g) e))

unfoldF' r (Abort (BRelease (0,0) f g) e) = ((mkProp e) `mkOr` (g `mkAbort`e))
unfoldF' r (Abort (BRelease (_,0) f g) e) = error "lower bound must not be greater than upper bound"
unfoldF' r (Abort (BRelease (0,u) f g) e) = ((mkProp e) `mkOr` ((g `mkAbort`e) `mkAnd` ((f `mkAbort`e) `mkOr` (mkNext (r ((mkBRelease (0,u-1) f g) `mkAbort` e))))))
unfoldF' r (Abort (BRelease (l,u) f g) e) = ((mkProp e) `mkOr` mkNext (mkAbort (mkBRelease (l-1,u-1) f g) e))

unfoldF' r (Abort (WBRelease (0,0) f g) e) = ((mkProp e) `mkOr` (g `mkAbort`e))
unfoldF' r (Abort (WBRelease (_,0) f g) e) = error "lower bound must not be greater than upper bound"
unfoldF' r (Abort (WBRelease (0,u) f g) e) = ((mkProp e) `mkOr` ((g `mkAbort`e) `mkAnd` ((f `mkAbort`e) `mkOr` (mkWNext (r ((mkWBRelease (0,u-1) f g) `mkAbort` e))))))
unfoldF' r (Abort (WBRelease (l,u) f g) e) = ((mkProp e) `mkOr` mkWNext (mkAbort (mkWBRelease (l-1,u-1) f g) e))

-- There is no unfolding for SImplies :-(
unfoldF' r f = f
-}
-------------------------------------------------------------------------------
-- PSL-Parser

formula :: (PSLFragment (reg prop), PSLFragment prop) => P.Parser (Formula reg prop)
formula = buildExpressionParser table prefixExpr
          P.<?> "PSL: formula"

atomicP :: (PSLFragment (reg prop), PSLFragment prop) => P.Parser (Formula reg prop)
atomicP = P.try (parser >>= return . mkWeakReg)
          P.<|> (reservedOp "\\strong" >> parser >>= return . mkStrongReg)
          P.<|> parens formula
          P.<?> "PSL: atomic expression"

-- Note: all prefix operator have highest precedence
-- buildExpressionParser does not allow for nesting of prefixes of same precedence.
-- Moreover it seems that nesting of lower precedence prefix operators in higher precedence
-- prefix operators does not work as well.  Seems that I do not understand something there ...
prefixExpr :: (PSLFragment (reg prop), PSLFragment prop) => P.Parser (Formula reg prop)
prefixExpr = P.try atomicP
             P.<|> prefix "\\not" mkNegate
             P.<|> pPrefix "\\BN" mkBNext
             P.<|> pPrefix "\\wBN" mkWBNext
             P.<|> prefix "\\N" mkNext
             P.<|> prefix "\\wN" mkWNext
             P.<|> pPrefix "\\BG" mkBGlobally
             P.<|> pPrefix "\\BF" mkBEventually
             P.<|> pPrefix "\\sBG" mkSBGlobally
             P.<|> pPrefix "\\wBF" mkWBEventually
             P.<|> prefix "\\G" mkGlobally
             P.<|> prefix "\\F" mkEventually
             P.<?> "PSL: prefix expression"
             where
             prefix name fun  = (reservedOp name >> prefixExpr >>= return . fun)
             pPrefix name fun = (reservedOp name >> do { b <- bound ; f <- prefixExpr ; return (fun b f) })

table :: (PSLFragment (reg prop), PSLFragment prop) => [[Operator Char () (Formula reg prop)]]
table = [ [binary "\\and" mkAnd AssocLeft]
        , [binary "\\or" mkOr AssocLeft]
        , [binary "\\implies" mkImplies AssocRight]
        , [binary "\\equiv" mkEquiv AssocLeft]

        , [pBinary "\\BU" mkBUntil AssocRight, pBinary "\\BR" mkBRelease AssocLeft]
        , [pBinary "\\BW" mkBWaitfor AssocRight, pBinary "\\sBR" mkSBRelease AssocLeft]
        , [binary "\\U" mkUntil AssocRight, binary "\\R" mkRelease AssocLeft]
        , [binary "\\W" mkWaitfor AssocRight, binary "\\sR" mkSRelease AssocLeft]

        , [abort]
        , [simplies]
        ]

-- TODO: better move simplies to pslexpr
binary name fun assoc  = Infix (reservedOp name >> return fun) assoc
pBinary name fun assoc = Infix (reservedOp name >> bound >>= return . fun) assoc
prefix name fun        = Prefix (reservedOp name >> return fun)
-- pPrefix name fun       = Prefix (reservedOp name >> bound >>= return . fun)
postfix name fun       = Postfix (reservedOp name >> return fun)

abort :: (PSLFragment (reg prop), PSLFragment prop) => Operator Char () (Formula reg prop)
abort                  = Postfix (reservedOp "\\abort" >> parser >>= return . (flip mkAbort))

simplies :: (PSLFragment (reg prop), PSLFragment prop) => Operator Char () (Formula reg prop)
simplies               = Prefix  ( P.try $ do { x <- parser; reservedOp "\\simplies"; return (mkSImplies x)} )

-- bounds
-- bound :: P.GenParser Char st a
bound = boundExpr

boundExpr = buildExpressionParser boundTable boundTerm

boundTerm = (parens boundExpr) P.<|> (parseOrdinal)

boundTable :: OperatorTable Char () Ordinal
boundTable = [ [prefix "-" negate, prefix "+" id]
             , [postfix "++" (+1)]
             , [binary "*" (*) AssocLeft {-,  binary "/" (div) AssocLeft-} ]
             , [binary "+" (+) AssocLeft, binary "-" (-)   AssocLeft]
             ]


text:
using System;
using System.Threading;
using System.Threading.Tasks;
using Microsoft.VisualStudio.TestTools.UnitTesting;
using Shouldly;
using Spect.Net.SpectrumEmu.Abstraction.Devices;
using Spect.Net.SpectrumEmu.Machine;
using Spect.Net.SpectrumEmu.Test.Helpers;

namespace Spect.Net.SpectrumEmu.Test.Devices.Screen
{
    [TestClass]
    public class ScreenDeviceTests
    {
        [TestMethod]
        public void UlaFrameTactCountIsCalculatedProperlyForSpectrum48Pal()
        {
            // --- Arrange
            var screenConfig = SpectrumModels.ZxSpectrum48Pal.Screen;
            var pixels = new TestPixelRenderer(screenConfig);
            var spectrum = new SpectrumAdvancedTestMachine(pixels, screenConfig);

            // --- Act
            var ulaFrameTactCount = spectrum.ScreenDevice.ScreenConfiguration.ScreenRenderingFrameTactCount;

            // --- Assert
            ulaFrameTactCount.ShouldBe(69888);
        }

        [TestMethod]
        public void RefreshRateIsCalculatedProperlyForSpectrum48Pal()
        {
            // --- Arrange
            var screenConfig = SpectrumModels.ZxSpectrum48Pal.Screen;
            var pixels = new TestPixelRenderer(screenConfig);
            var spectrum = new SpectrumAdvancedTestMachine(pixels, screenConfig);

            // --- Act
            var freq = Math.Round(spectrum.ScreenDevice.RefreshRate, 2);

            // --- Assert
            freq.ShouldBe(50.08m);
        }

        [TestMethod]
        public void FlashToggleRateIsCalculatedProperlyForSpectrum48Pal()
        {
            // --- Arrange
            var screenConfig = SpectrumModels.ZxSpectrum48Pal.Screen;
            var pixels = new TestPixelRenderer(screenConfig);
            var spectrum = new SpectrumAdvancedTestMachine(pixels, screenConfig);

            // --- Act
            var rate = spectrum.ScreenDevice.FlashToggleFrames;

            // --- Assert
            rate.ShouldBe(25);
        }

        [TestMethod]
        public void UlaFrameTactCountIsCalculatedProperlyForSpectrum48Ntsc()
        {
            // --- Arrange
            var screenConfig = SpectrumModels.ZxSpectrum48Ntsc.Screen;
            var pixels = new TestPixelRenderer(screenConfig);
            var spectrum = new SpectrumAdvancedTestMachine(pixels, screenConfig);

            // --- Act
            var ulaFrameTactCount = spectrum.ScreenDevice.ScreenConfiguration.ScreenRenderingFrameTactCount;

            // --- Assert
            ulaFrameTactCount.ShouldBe(59136);
        }

        [TestMethod]
        public void RefreshRateIsCalculatedProperlyForSpectrum48Ntsc()
        {
            // --- Arrange
            var screenConfig = SpectrumModels.ZxSpectrum48Ntsc.Screen;
            var pixels = new TestPixelRenderer(screenConfig);
            var spectrum = new SpectrumAdvancedTestMachine(pixels, screenConfig);

            // --- Act
            var freq = Math.Round(spectrum.ScreenDevice.RefreshRate, 2);

            // --- Assert
            freq.ShouldBe(59.19m);
        }

        [TestMethod]
        public void FlashToggleRateIsCalculatedProperlyForSpectrum48Ntsc()
        {
            // --- Arrange
            var screenConfig = SpectrumModels.ZxSpectrum48Ntsc.Screen;
            var pixels = new TestPixelRenderer(screenConfig);
            var spectrum = new SpectrumAdvancedTestMachine(pixels, screenConfig);

            // --- Act
            var rate = spectrum.ScreenDevice.FlashToggleFrames;

            // --- Assert
            rate.ShouldBe(30);
        }

        [TestMethod]
        public void UlaFrameTactCountIsCalculatedProperlyForSpectrum128Pal()
        {
            // --- Arrange
            var screenConfig = SpectrumModels.ZxSpectrum128Pal.Screen;
            var pixels = new TestPixelRenderer(screenConfig);
            var spectrum = new SpectrumAdvancedTestMachine(pixels, screenConfig);

            // --- Act
            var ulaFrameTactCount = spectrum.ScreenDevice.ScreenConfiguration.ScreenRenderingFrameTactCount;

            // --- Assert
            ulaFrameTactCount.ShouldBe(70908);
        }

        [TestMethod]
        public void RefreshRateIsCalculatedProperlyForSpectrum128Pal()
        {
            // --- Arrange
            var screenConfig = SpectrumModels.ZxSpectrum128Pal.Screen;
            var cpuConfig = SpectrumModels.ZxSpectrum128Pal.Cpu;
            var pixels = new TestPixelRenderer(screenConfig);
            var spectrum = new SpectrumAdvancedTestMachine(pixels, screenConfig, cpuConfig);

            // --- Act
            var freq = Math.Round(spectrum.ScreenDevice.RefreshRate, 2);

            // --- Assert
            freq.ShouldBe(50.02m);
        }

        [TestMethod]
        public void FlashToggleRateIsCalculatedProperlyForSpectrum128Pal()
        {
            // --- Arrange
            var screenConfig = SpectrumModels.ZxSpectrum128Pal.Screen;
            var cpuConfig = SpectrumModels.ZxSpectrum128Pal.Cpu;
            var pixels = new TestPixelRenderer(screenConfig);
            var spectrum = new SpectrumAdvancedTestMachine(pixels, screenConfig, cpuConfig);

            // --- Act
            var rate = spectrum.ScreenDevice.FlashToggleFrames;

            // --- Assert
            rate.ShouldBe(25);
        }

        [TestMethod]
        public void SettingBorderValueDoesNotChangeInvisibleScreenArea()
        {
            // --- Arrange
            var pixels = new TestPixelRenderer(SpectrumModels.ZxSpectrum48Pal.Screen);
            var spectrum = new SpectrumAdvancedTestMachine(pixels);

            // --- Because we execute only 451 CPU tacts, rendering does not
            // --- reach the visible border area
            spectrum.InitCode(new byte[]
            {
                0xF3,             // DI
                0x3E, 0x05,       // LD A,$05
                0xD3, 0xFE,       // OUT ($FE),A
                0x01, 0x10, 0x00, // LD BC,$0010
                0x0B,             // DECLB: DEC BC
                0x78,             // LD A,B
                0xB1,             // OR C
                0x20, 0xFB,       // JR NZ,DECLB
                0xFB,             // EI
                0x76              // HALT
            });
            ((IScreenDeviceTestSupport)spectrum.ScreenDevice).FillScreenBuffer(0xFF);

            // --- Act
            spectrum.ExecuteCycle(CancellationToken.None, new ExecuteCycleOptions(EmulationMode.UntilHalt));

            // --- Assert
            var regs = spectrum.Cpu.Registers;
            regs.PC.ShouldBe((ushort)0x800E);
            spectrum.Cpu.Tacts.ShouldBe(451L);
            pixels.IsFrameReady.ShouldBeFalse();

            pixels.SetPixelMemory(spectrum.ScreenDevice.GetPixelBuffer());
            for (var row = 0; row < spectrum.ScreenDevice.ScreenConfiguration.ScreenLines; row++)
            {
                for (var column = 0; column < spectrum.ScreenDevice.ScreenConfiguration.ScreenWidth; column++)
                {
                    pixels[row, column].ShouldBe((byte)0xFF);
                }
            }
        }

        [TestMethod]
        public void SettingBorderValueChangesBorderArea1()
        {
            // --- Arrange
            var pixels = new TestPixelRenderer(SpectrumModels.ZxSpectrum48Pal.Screen);
            var spectrum = new SpectrumAdvancedTestMachine(pixels);

            // --- Because we execute 3675 CPU tacts, rendering reaches
            // --- the first 104 pixels of the first border row
            spectrum.InitCode(new byte[]
            {
                0xF3,             // DI
                0x3E, 0x05,       // LD A,$05
                0xD3, 0xFE,       // OUT ($FE),A
                0x01, 0x8C, 0x00, // LD BC,$008C
                0x0B,             // DECLB: DEC BC
                0x78,             // LD A,B
                0xB1,             // OR C
                0x20, 0xFB,       // JR NZ,DECLB
                0x76              // HALT
            });

            // --- Act
            spectrum.ExecuteCycle(CancellationToken.None, new ExecuteCycleOptions(EmulationMode.UntilHalt));

            // --- Assert
            var regs = spectrum.Cpu.Registers;
            regs.PC.ShouldBe((ushort)0x800D);
            spectrum.Cpu.Tacts.ShouldBe(3671L);
            pixels.IsFrameReady.ShouldBeFalse();

            // --- The left 176 pixels of the first border row should be set to 0x05
            pixels.SetPixelMemory(spectrum.ScreenDevice.GetPixelBuffer());
            for (var column = 0; column < 176; column++)
            {
                pixels[0, column].ShouldBe((byte)0x05);
            }

            // --- The remaining pixels of the first border row should be intact (0xFF)
            for (var column = 176; column < spectrum.ScreenDevice.ScreenConfiguration.ScreenWidth; column++)
            {
                pixels[0, column].ShouldBe((byte)0x00);
            }

            // --- All the other screen bytes should be intact (0xFF)
            for (var row = 1; row < spectrum.ScreenDevice.ScreenConfiguration.ScreenLines; row++)
            {
                for (var column = 0; column < spectrum.ScreenDevice.ScreenConfiguration.ScreenWidth; column++)
                {
                    pixels[row, column].ShouldBe((byte)0x00);
                }
            }
        }

        [TestMethod]
        public void SettingBorderValueChangesBorderArea2()
        {
            // --- Arrange
            var pixels = new TestPixelRenderer(SpectrumModels.ZxSpectrum48Pal.Screen);
            var spectrum = new SpectrumAdvancedTestMachine(pixels);

            // --- Because we execute 14335 CPU tacts, rendering reaches
            // --- all top border rows, save the last invisible pixels of the last top border row
            spectrum.InitCode(new byte[]
            {
                0xF3,             // DI
                0x3E, 0x05,       // LD A,$05
                0xD3, 0xFE,       // OUT ($FE),A
                0x01, 0x26, 0x02, // LD BC,$0226
                0x0B,             // DECLB: DEC BC
                0x78,             // LD A,B
                0xB1,             // OR C
                0x20, 0xFB,       // JR NZ,DECLB
                0x76              // HALT
            });

            // --- Act
            spectrum.ExecuteCycle(CancellationToken.None, new ExecuteCycleOptions(EmulationMode.UntilHalt));

            // --- Assert
            var regs = spectrum.Cpu.Registers;
            regs.PC.ShouldBe((ushort)0x800D);
            spectrum.Cpu.Tacts.ShouldBe(14331L);
            pixels.IsFrameReady.ShouldBeFalse();

            // --- The top 48 border rows should be set to 0x05
            pixels.SetPixelMemory(spectrum.ScreenDevice.GetPixelBuffer());
            for (var row = 0; row < 48 ; row++)
            {
                for (var column = 0; column < spectrum.ScreenDevice.ScreenConfiguration.ScreenWidth; column++)
                {
                    pixels[row, column].ShouldBe((byte)0x05);
                }
            }

            // --- All the other screen bytes should be intact (0xFF)
            for (var row = 48; row < spectrum.ScreenDevice.ScreenConfiguration.ScreenLines; row++)
            {
                for (var column = 0; column < spectrum.ScreenDevice.ScreenConfiguration.ScreenWidth; column++)
                {
                    pixels[row, column].ShouldBe((byte)0x00);
                }
            }
        }

        [TestMethod]
        public void SettingBorderValueChangesBorderArea3()
        {
            // --- Arrange
            var pixels = new TestPixelRenderer(SpectrumModels.ZxSpectrum48Pal.Screen);
            var spectrum = new SpectrumAdvancedTestMachine(pixels);

            // --- Because we execute 14413 CPU tacts, rendering reaches
            // --- all top border rows + the left border of the first
            // --- display row, and sets the first 28 pixels to 0.

            spectrum.InitCode(new byte[]
            {
                0xF3,             // DI
                0x3E, 0x05,       // LD A,$05
                0xD3, 0xFE,       // OUT ($FE),A
                0x01, 0x29, 0x02, // LD BC,$0229
                0x0B,             // DECLB: DEC BC
                0x78,             // LD A,B
                0xB1,             // OR C
                0x20, 0xFB,       // JR NZ,DECLB
                0xFB,             // EI
                0x76              // HALT
            });
            ((IScreenDeviceTestSupport)spectrum.ScreenDevice).FillScreenBuffer(0xDC);

            // --- Act
            spectrum.ExecuteCycle(CancellationToken.None, new ExecuteCycleOptions(EmulationMode.UntilHalt));

            // --- Assert
            var regs = spectrum.Cpu.Registers;
            regs.PC.ShouldBe((ushort)0x800E);
            spectrum.Cpu.Tacts.ShouldBe(14413L);
            pixels.IsFrameReady.ShouldBeFalse();

            // --- The top 48 border rows should be set to 0x05
            pixels.SetPixelMemory(spectrum.ScreenDevice.GetPixelBuffer());
            for (var row = 0; row < 48; row++)
            {
                for (var column = 0; column < spectrum.ScreenDevice.ScreenConfiguration.ScreenWidth; column++)
                {
                    pixels[row, column].ShouldBe((byte)0x05);
                }
            }

            // --- The left border of row 48 should be set to 0x05
            for (var column = 0; column < 48; column++)
            {
                pixels[48, column].ShouldBe((byte)0x05);
            }

            // --- The first 12 pixels of the first display row (48) should be set to 0
            for (var column = 48; column < 156; column++)
            {
                pixels[48, column].ShouldBe((byte)0x00);
            }

            // --- The other pixels of the first display row (48) should be intact
            for (var column = 156; column < spectrum.ScreenDevice.ScreenConfiguration.ScreenWidth; column++)
            {
                pixels[48, column].ShouldBe((byte)0xDC);
            }

            // --- All the other screen bytes should be intact (0xDC)
            for (var row = 49; row < spectrum.ScreenDevice.ScreenConfiguration.ScreenLines; row++)
            {
                for (var column = 0; column < spectrum.ScreenDevice.ScreenConfiguration.ScreenWidth; column++)
                {
                    pixels[row, column].ShouldBe((byte)0xDC);
                }
            }
        }

        [TestMethod]
        public void RenderingScreenWithEmptyPixelsWorks()
        {
            // --- Arrange
            var pixels = new TestPixelRenderer(SpectrumModels.ZxSpectrum48Pal.Screen);
            var spectrum = new SpectrumAdvancedTestMachine(pixels);

            // --- Because we execute 69637 CPU tacts, rendering set all border
            // --- pixels to 5 + screen pixels to 0
            spectrum.InitCode(new byte[]
            {
                0xF3,             // DI
                0x3E, 0x05,       // LD A,$05
                0xD3, 0xFE,       // OUT ($FE),A
                0x01, 0x75, 0x0A, // LD BC,$0A75
                0x0B,             // DECLB: DEC BC
                0x78,             // LD A,B
                0xB1,             // OR C
                0x20, 0xFB,       // JR NZ,DECLB
                0x76              // HALT
            });

            // --- Act
            spectrum.ExecuteCycle(CancellationToken.None, new ExecuteCycleOptions(EmulationMode.UntilHalt));

            // --- Assert
            var regs = spectrum.Cpu.Registers;
            regs.PC.ShouldBe((ushort)0x800D);
            spectrum.Cpu.Tacts.ShouldBe(69633L);
            pixels.IsFrameReady.ShouldBeFalse();

            // --- The top 48 border rows should be set to 0x05
            pixels.SetPixelMemory(spectrum.ScreenDevice.GetPixelBuffer());
            for (var row = 0; row < 48; row++)
            {
                for (var column = 0; column < spectrum.ScreenDevice.ScreenConfiguration.ScreenWidth; column++)
                {
                    pixels[row, column].ShouldBe((byte)0x05);
                }
            }

            // --- Display rows should have a border value of 0x05 and a pixel value of 0x00
            for (var row = 48; row < 48 + 192; row++)
            {
                for (var column = 0; column < spectrum.ScreenDevice.ScreenConfiguration.BorderLeftPixels; column++)
                {
                    pixels[row, column].ShouldBe((byte)0x05);
                }
                for (var column = spectrum.ScreenDevice.ScreenConfiguration.BorderLeftPixels;
                    column < spectrum.ScreenDevice.ScreenConfiguration.ScreenWidth - spectrum.ScreenDevice.ScreenConfiguration.BorderRightPixels;
                    column++)
                {
                    pixels[row, column].ShouldBe((byte)0x00);
                }
                for (var column = spectrum.ScreenDevice.ScreenConfiguration.ScreenWidth - spectrum.ScreenDevice.ScreenConfiguration.BorderRightPixels;
                    column < spectrum.ScreenDevice.ScreenConfiguration.ScreenWidth;
                    column++)
                {
                    pixels[row, column].ShouldBe((byte)0x05);
                }
            }

            // --- The bottom 48 border rows should be set to 0x05
            for (var row = 48 + 192; row < spectrum.ScreenDevice.ScreenConfiguration.ScreenLines; row++)
            {
                for (var column = 0; column < spectrum.ScreenDevice.ScreenConfiguration.ScreenWidth; column++)
                {
                    pixels[row, column].ShouldBe((byte)0x05);
                }
            }
        }

        [TestMethod]
        public void RenderingScreenWithPatternWorks1()
        {
            // --- Arrange
            var pixels = new TestPixelRenderer(SpectrumModels.ZxSpectrum48Pal.Screen);
            var spectrum = new SpectrumAdvancedTestMachine(pixels);

            // --- We render the screen with pixels with color index
            // --- of 0x09 and 0x0A in a chequered pattern
            spectrum.InitCode(new byte[]
            {
                0xF3,             // DI
                0x3E, 0x05,       // LD A,$05
                0xD3, 0xFE,       // OUT ($FE),A
                0x01, 0x75, 0x0A, // LD BC,$0A75
                0x0B,             // DECLB: DEC BC
                0x78,             // LD A,B
                0xB1,             // OR C
                0x20, 0xFB,       // JR NZ,DECLB
                0x76              // HALT
            });

            for (var addr = 0x4000; addr < 0x5800; addr++)
            {
                spectrum.WriteSpectrumMemory((ushort)addr, (byte)((addr & 0x0100) == 0 ? 0x55 : 0xAA));
            }
            for (var addr = 0x5800; addr < 0x5B00; addr++)
            {
                spectrum.WriteSpectrumMemory((ushort)addr, 0x51);
            }

            // --- Act
            spectrum.ExecuteCycle(CancellationToken.None, new ExecuteCycleOptions(EmulationMode.UntilHalt));

            // --- Assert
            var regs = spectrum.Cpu.Registers;
            regs.PC.ShouldBe((ushort)0x800D);
            spectrum.Cpu.Tacts.ShouldBe(69633L);
            pixels.IsFrameReady.ShouldBeFalse();

            // --- The top 48 border rows should be set to 0x05
            pixels.SetPixelMemory(spectrum.ScreenDevice.GetPixelBuffer());
            for (var row = 0; row < 48; row++)
            {
                for (var column = 0; column < spectrum.ScreenDevice.ScreenConfiguration.ScreenWidth; column++)
                {
                    pixels[row, column].ShouldBe((byte)0x05);
                }
            }

            // --- Display rows should have a border value of 0x05 and a pixel value of 0x00
            for (var row = 48; row < 48 + 192; row++)
            {
                for (var column = 0; column < spectrum.ScreenDevice.ScreenConfiguration.BorderLeftPixels; column++)
                {
                    pixels[row, column].ShouldBe((byte)0x05);
                }
                for (var column = spectrum.ScreenDevice.ScreenConfiguration.BorderLeftPixels;
                    column < spectrum.ScreenDevice.ScreenConfiguration.ScreenWidth - spectrum.ScreenDevice.ScreenConfiguration.BorderRightPixels;
                    column++)
                {
                    var expectedColor = (row + column) % 2 == 1  ? 0x09 : 0x0A;
                    pixels[row, column].ShouldBe((byte)expectedColor);
                }
                for (var column = spectrum.ScreenDevice.ScreenConfiguration.ScreenWidth - spectrum.ScreenDevice.ScreenConfiguration.BorderRightPixels;
                    column < spectrum.ScreenDevice.ScreenConfiguration.ScreenWidth;
                    column++)
                {
                    pixels[row, column].ShouldBe((byte)0x05);
                }
            }

            // --- The bottom 48 border rows should be set to 0x05
            for (var row = 48 + 192; row < spectrum.ScreenDevice.ScreenConfiguration.ScreenLines; row++)
            {
                for (var column = 0; column < spectrum.ScreenDevice.ScreenConfiguration.ScreenWidth; column++)
                {
                    pixels[row, column].ShouldBe((byte)0x05);
                }
            }
        }

        [TestMethod]
        public void RenderingScreenWithUntilFrameEnds()
        {
            // --- Arrange
            var pixels = new TestPixelRenderer(SpectrumModels.ZxSpectrum48Pal.Screen);
            var spectrum = new SpectrumAdvancedTestMachine(pixels);

            // === The same as RenderingScreenWithPatternWorks1 test case, but waits
            // === while the full frame is rendered.

            // --- We render the screen with pixels with color index
            // --- of 0x09 and 0x0A in a chequered pattern
            spectrum.InitCode(new byte[]
            {
                0xF3,             // DI
                0x3E, 0x05,       // LD A,$05
                0xD3, 0xFE,       // OUT ($FE),A
                0x01, 0x75, 0x0A, // LD BC,$0A75
                0x0B,             // DECLB: DEC BC
                0x78,             // LD A,B
                0xB1,             // OR C
                0x20, 0xFB,       // JR NZ,DECLB
                0x76              // HALT
            });

            for (var addr = 0x4000; addr < 0x5800; addr++)
            {
                spectrum.WriteSpectrumMemory((ushort)addr, (byte)((addr & 0x0100) == 0 ? 0x55 : 0xAA));
            }
            for (var addr = 0x5800; addr < 0x5B00; addr++)
            {
                spectrum.WriteSpectrumMemory((ushort)addr, 0x51);
            }
            var startTime = spectrum.Clock.GetCounter();

            // --- Act
            // === Be aware of EmulationMode.UntilFrameEnds
            spectrum.ExecuteCycle(CancellationToken.None, new ExecuteCycleOptions(EmulationMode.UntilFrameEnds));

            // === Display some extra information about the duration of the frame execution
            var duration = (spectrum.Clock.GetCounter() - startTime)
                /(double)spectrum.Clock.GetFrequency();
            Console.WriteLine("Frame execution time: {0} second", duration);

            // --- Assert
            var regs = spectrum.Cpu.Registers;
            regs.PC.ShouldBe((ushort)0x800D);
            pixels.IsFrameReady.ShouldBeTrue();

            // === The full frame's tact time is used
            spectrum.Cpu.Tacts.ShouldBeGreaterThanOrEqualTo(spectrum.ScreenDevice.ScreenConfiguration.ScreenRenderingFrameTactCount);

            // === The full time should not exceed the frame time + the longest Z80 instruction length,
            // === which is 23
            spectrum.Cpu.Tacts.ShouldBeLessThanOrEqualTo(spectrum.ScreenDevice.ScreenConfiguration.ScreenRenderingFrameTactCount + 23);

            // --- The top 48 border rows should be set to 0x05
            pixels.SetPixelMemory(spectrum.ScreenDevice.GetPixelBuffer());
            for (var row = 0; row < 48; row++)
            {
                for (var column = 0; column < spectrum.ScreenDevice.ScreenConfiguration.ScreenWidth; column++)
                {
                    pixels[row, column].ShouldBe((byte)0x05);
                }
            }

            // --- Display rows should have a border value of 0x05 and a pixel value of 0x00
            for (var row = 48; row < 48 + 192; row++)
            {
                for (var column = 0; column < spectrum.ScreenDevice.ScreenConfiguration.BorderLeftPixels; column++)
                {
                    pixels[row, column].ShouldBe((byte)0x05);
                }
                for (var column = spectrum.ScreenDevice.ScreenConfiguration.BorderLeftPixels;
                    column < spectrum.ScreenDevice.ScreenConfiguration.ScreenWidth - spectrum.ScreenDevice.ScreenConfiguration.BorderRightPixels;
                    column++)
                {
                    var expectedColor = (row + column) % 2 == 1 ? 0x09 : 0x0A;
                    pixels[row, column].ShouldBe((byte)expectedColor);
                }
                for (var column = spectrum.ScreenDevice.ScreenConfiguration.ScreenWidth - spectrum.ScreenDevice.ScreenConfiguration.BorderRightPixels;
                    column < spectrum.ScreenDevice.ScreenConfiguration.ScreenWidth;
                    column++)
                {
                    pixels[row, column].ShouldBe((byte)0x05);
                }
            }

            // --- The bottom 48 border rows should be set to 0x05
            for (var row = 48 + 192; row < spectrum.ScreenDevice.ScreenConfiguration.ScreenLines; row++)
            {
                for (var column = 0; column < spectrum.ScreenDevice.ScreenConfiguration.ScreenWidth; column++)
                {
                    pixels[row, column].ShouldBe((byte)0x05);
                }
            }
        }

        [TestMethod]
        public void RenderingScreenWithUntilNewFrameStarts()
        {
            // --- Arrange
            var pixels = new TestPixelRenderer(SpectrumModels.ZxSpectrum48Pal.Screen);
            var spectrum = new SpectrumAdvancedTestMachine(pixels);

            // === The same as RenderingScreenWithPatternWorks1 test case, but waits
            // === while the full frame is rendered and a new frame is started.

            // --- We render the screen with pixels with color index
            // --- of 0x09 and 0x0A in a chequered pattern
            spectrum.InitCode(new byte[]
            {
                0xF3,             // DI
                0x3E, 0x05,       // LD A,$05
                0xD3, 0xFE,       // OUT ($FE),A
                0x01, 0x75, 0x0A, // LD BC,$0A75
                0x0B,             // DECLB: DEC BC
                0x78,             // LD A,B
                0xB1,             // OR C
                0x20, 0xFB,       // JR NZ,DECLB
                0x76              // HALT
            });

            for (var addr = 0x4000; addr < 0x5800; addr++)
            {
                spectrum.WriteSpectrumMemory((ushort)addr, (byte)((addr & 0x0100) == 0 ? 0x55 : 0xAA));
            }
            for (var addr = 0x5800; addr < 0x5B00; addr++)
            {
                spectrum.WriteSpectrumMemory((ushort)addr, 0x51);
            }
            var startTime = spectrum.Clock.GetCounter();

            // --- Act
            // === Be aware of EmulationMode.UntilNextFrame
            spectrum.ExecuteCycle(CancellationToken.None, new ExecuteCycleOptions(EmulationMode.UntilFrameEnds));

            // === Display some extra information about the duration of the frame execution
            var duration = (spectrum.Clock.GetCounter() - startTime)
                / (double)spectrum.Clock.GetFrequency();
            Console.WriteLine("Frame execution time: {0} second", duration);

            // --- Assert
            var regs = spectrum.Cpu.Registers;
            regs.PC.ShouldBe((ushort)0x800D);
            pixels.IsFrameReady.ShouldBeTrue();

            // === The full frame's tact time is used
            spectrum.Cpu.Tacts.ShouldBeGreaterThanOrEqualTo(spectrum.ScreenDevice.ScreenConfiguration.ScreenRenderingFrameTactCount);

            // === The full time should not exceed the frame time + the longest Z80 instruction length,
            // === which is 23
            spectrum.Cpu.Tacts.ShouldBeLessThanOrEqualTo(spectrum.ScreenDevice.ScreenConfiguration.ScreenRenderingFrameTactCount + 23);

            // --- The top 48 border rows should be set to 0x05
            pixels.SetPixelMemory(spectrum.ScreenDevice.GetPixelBuffer());
            for (var row = 0; row < 48; row++)
            {
                for (var column = 0; column < spectrum.ScreenDevice.ScreenConfiguration.ScreenWidth; column++)
                {
                    pixels[row, column].ShouldBe((byte)0x05);
                }
            }

            // --- Display rows should have a border value of 0x05 and a pixel value of 0x00
            for (var row = 48; row < 48 + 192; row++)
            {
                for (var column = 0; column < spectrum.ScreenDevice.ScreenConfiguration.BorderLeftPixels; column++)
                {
                    pixels[row, column].ShouldBe((byte)0x05);
                }
                for (var column = spectrum.ScreenDevice.ScreenConfiguration.BorderLeftPixels;
                    column < spectrum.ScreenDevice.ScreenConfiguration.ScreenWidth - spectrum.ScreenDevice.ScreenConfiguration.BorderRightPixels;
                    column++)
                {
                    var expectedColor = (row + column) % 2 == 1 ? 0x09 : 0x0A;
                    pixels[row, column].ShouldBe((byte)expectedColor);
                }
                for (var column = spectrum.ScreenDevice.ScreenConfiguration.ScreenWidth - spectrum.ScreenDevice.ScreenConfiguration.BorderRightPixels;
                    column < spectrum.ScreenDevice.ScreenConfiguration.ScreenWidth;
                    column++)
                {
                    pixels[row, column].ShouldBe((byte)0x05);
                }
            }

            // --- The bottom 48 border rows should be set to 0x05
            for (var row = 48 + 192; row < spectrum.ScreenDevice.ScreenConfiguration.ScreenLines; row++)
            {
                for (var column = 0; column < spectrum.ScreenDevice.ScreenConfiguration.ScreenWidth; column++)
                {
                    pixels[row, column].ShouldBe((byte)0x05);
                }
            }
        }

        [TestMethod]
        public void RenderingTenScreenFramesWorksAsExpected()
        {
            // --- Arrange
            var pixels = new TestPixelRenderer(SpectrumModels.ZxSpectrum48Pal.Screen);
            var spectrum = new SpectrumAdvancedTestMachine(pixels);

            // === The same as RenderingScreenWithPatternWorks1 test case, but waits
            // === while the full frame is rendered and a new frame is started.

            // --- We render the screen with pixels with color index
            // --- of 0x09 and 0x0A in a chequered pattern
            spectrum.InitCode(new byte[]
            {
                0xF3,             // DI
                0x3E, 0x05,       // LD A,$05
                0xD3, 0xFE,       // OUT ($FE),A
                0x01, 0x75, 0x0A, // LD BC,$0A75
                0x0B,             // DECLB: DEC BC
                0x78,             // LD A,B
                0xB1,             // OR C
                0x20, 0xFB,       // JR NZ,DECLB
                0x76              // HALT
            });

            for (var addr = 0x4000; addr < 0x5800; addr++)
            {
                spectrum.WriteSpectrumMemory((ushort)addr, (byte)((addr & 0x0100) == 0 ? 0x55 : 0xAA));
            }
            for (var addr = 0x5800; addr < 0x5B00; addr++)
            {
                spectrum.WriteSpectrumMemory((ushort)addr, 0x51);
            }
            var startTime = spectrum.Clock.GetCounter();

            // --- Act
            // === Be aware of EmulationMode.UntilNextFrame
            for (var i = 0; i < 10; i++)
            {
                spectrum.ExecuteCycle(CancellationToken.None, new ExecuteCycleOptions(EmulationMode.UntilFrameEnds));
            }

            // === Display some extra information about the duration of the frame execution
            var duration = (spectrum.Clock.GetCounter() - startTime)
                / (double)spectrum.Clock.GetFrequency();
            Console.WriteLine("Frame execution time: {0} second", duration);

            // --- Assert
            var regs = spectrum.Cpu.Registers;
            regs.PC.ShouldBe((ushort)0x800D);
            pixels.IsFrameReady.ShouldBeTrue();

            // === The full frame's tact time is used
            spectrum.Cpu.Tacts.ShouldBeGreaterThanOrEqualTo(spectrum.ScreenDevice.ScreenConfiguration.ScreenRenderingFrameTactCount*10);

            // === The full time should not exceed the 10*frame time + the longest Z80 instruction length,
            // === which is 23
            spectrum.Cpu.Tacts.ShouldBeLessThanOrEqualTo(spectrum.ScreenDevice.ScreenConfiguration.ScreenRenderingFrameTactCount*10 + 23);

            // --- The top 48 border rows should be set to 0x05
            pixels.SetPixelMemory(spectrum.ScreenDevice.GetPixelBuffer());
            for (var row = 0; row < 48; row++)
            {
                for (var column = 0; column < spectrum.ScreenDevice.ScreenConfiguration.ScreenWidth; column++)
                {
                    pixels[row, column].ShouldBe((byte)0x05);
                }
            }

            // --- Display rows should have a border value of 0x05 and a pixel value of 0x00
            for (var row = 48; row < 48 + 192; row++)
            {
                for (var column = 0; column < spectrum.ScreenDevice.ScreenConfiguration.BorderLeftPixels; column++)
                {
                    pixels[row, column].ShouldBe((byte)0x05);
                }
                for (var column = spectrum.ScreenDevice.ScreenConfiguration.BorderLeftPixels;
                    column < spectrum.ScreenDevice.ScreenConfiguration.ScreenWidth - spectrum.ScreenDevice.ScreenConfiguration.BorderRightPixels;
                    column++)
                {
                    var expectedColor = (row + column) % 2 == 1 ? 0x09 : 0x0A;
                    pixels[row, column].ShouldBe((byte)expectedColor);
                }
                for (var column = spectrum.ScreenDevice.ScreenConfiguration.ScreenWidth - spectrum.ScreenDevice.ScreenConfiguration.BorderRightPixels;
                    column < spectrum.ScreenDevice.ScreenConfiguration.ScreenWidth;
                    column++)
                {
                    pixels[row, column].ShouldBe((byte)0x05);
                }
            }

            // --- The bottom 48 border rows should be set to 0x05
            for (var row = 48 + 192; row < spectrum.ScreenDevice.ScreenConfiguration.ScreenLines; row++)
            {
                for (var column = 0; column < spectrum.ScreenDevice.ScreenConfiguration.ScreenWidth; column++)
                {
                    pixels[row, column].ShouldBe((byte)0x05);
                }
            }
        }

        [TestMethod]
        public void ExecutionCyleWorksWithCancellation()
        {
            // --- Arrange
            var pixels = new TestPixelRenderer(SpectrumModels.ZxSpectrum48Pal.Screen);
            var spectrum = new SpectrumAdvancedTestMachine(pixels);

            // === The same as RenderingScreenWithPatternWorks1 test case, but waits
            // === while the full frame is rendered and a new frame is started.

            // --- We render the screen with pixels with color index
            // --- of 0x09 and 0x0A in a chequered pattern
            spectrum.InitCode(new byte[]
            {
                0xF3,             // DI
                0x3E, 0x05,       // LD A,$05
                0xD3, 0xFE,       // OUT ($FE),A
                0x01, 0x75, 0x0A, // LD BC,$0A75
                0x0B,             // DECLB: DEC BC
                0x78,             // LD A,B
                0xB1,             // OR C
                0x20, 0xFB,       // JR NZ,DECLB
                0xFB,             // EI
                0x76              // HALT
            });

            for (var addr = 0x4000; addr < 0x5800; addr++)
            {
                spectrum.WriteSpectrumMemory((ushort)addr, (byte)((addr & 0x0100) == 0 ? 0x55 : 0xAA));
            }
            for (var addr = 0x5800; addr < 0x5B00; addr++)
            {
                spectrum.WriteSpectrumMemory((ushort)addr, 0x51);
            }
            var counter = spectrum.Clock.GetCounter();
            var cancellationTime = counter + spectrum.Clock.GetFrequency()/100000; // 0.01ms

            var startTime = spectrum.Clock.GetCounter();
            var cancellationSource = new CancellationTokenSource();

            // --- Act
            // === We wait up to two frames
            Task.WaitAll(
                Task.Run(() => spectrum.ExecuteCycle(cancellationSource.Token, new ExecuteCycleOptions(EmulationMode.UntilFrameEnds)),
                    cancellationSource.Token),
                Task.Run(() =>
                {
                    spectrum.Clock.WaitUntil(cancellationTime, cancellationSource.Token);
                    cancellationSource.Cancel();
                }, cancellationSource.Token));

            // === Display some extra information about the duration of the frame execution
            var duration = (spectrum.Clock.GetCounter() - startTime)
                / (double)spectrum.Clock.GetFrequency();
            Console.WriteLine("Frame execution time: {0} second", duration);

            // --- Assert
            // === Only a part of the frame's tact time is used
            spectrum.Cpu.Tacts.ShouldBeLessThanOrEqualTo(spectrum.ScreenDevice.ScreenConfiguration.ScreenRenderingFrameTactCount + 1);
        }
    }
}


text:
#ifndef __UTIL_H
#define __UTIL_H

// #include <pthread.h>
// #include <sys/time.h>
#include <errno.h>
#include <string>

#include "MaceTypes.h"
#include "Exception.h"

#include "mstring.h"
// #include "RandomUtil.h"
// #include "TimeUtil.h"

/**
 * \file Util.h
 * \brief defines the Util utility methods
 */

/**
 * \addtogroup Utils
 * \brief Mace contains a variety of Util classes.  Each contains a set of
 * static public methods to help with a variety of tasks.  The functions are
 * broken up into categories, each implemented in a separate class and file.
 * @{
 */

/**
 * \brief a set of basic non-categories utilities.
 *
 * Most of these have to do with DNS, MaceAddr, SockAddr, and error strings
 */
class Util {
public:
  static const uint16_t DEFAULT_MACE_PORT = 5377; ///< The default port if none is provided
  static const bool REPLAY; ///< UNUSED.  Designed for a flag indicating replay.

public:
  static const MaceAddr& getMaceAddr() throw (AddressException); ///< method to get the local MaceAddr
  static int getAddr() throw (AddressException); ///< method to get the local ipaddress as a packed int
  // this will return the packed ip address of the hostname, which
  // could also be an ip address in dotted notation
  static int getAddr(const std::string& hostname) throw (AddressException); ///< method to convert a string (ip or hostname) into a packed int IP.
  static uint16_t getPort(); ///< return the default port (params::MACE_PORT, the port from params::MACE_LOCAL_ADDRESS, or the DEFAULT_MACE_PORT otherwise)
  static int getHostByName(const std::string& hostname) throw (AddressException); ///< equivalent to getAddr(const std::string&)
  static MaceAddr getMaceAddr(const std::string& hostname) throw (AddressException); ///< translate the address string into a MaceAddr
  static std::string getHostname(); ///< return the local hostname
  /**
   * Private IPs are one of
   * - 10.0.0.0        -   10.255.255.255  (10/8 prefix)
   * - 172.16.0.0      -   172.31.255.255  (172.16/12 prefix)
   * - 192.168.0.0     -   192.168.255.255 (192.168/16 prefix)
   */
  static bool isPrivateAddr(uint32_t a); ///< takes a packed int, determines if it is a private IP.
  static bool isHostReachable(const MaceKey& k); ///< either params::MACE_ALL_HOSTS_REACHABLE, or address has either a valid proxy or local address
  /// returns the hostname of the key if the host can be directly routed to.
  /**
   * throws an UnreachablePrivateAddressException if the
   * host can only be reached through the proxy address
   */
  static std::string getHostname(const MaceKey& k) throw (AddressException);
  static std::string getHostname(const std::string& ipaddr) throw (AddressException); ///< return the hostname of the IP address
  static std::string getHostname(int ipaddr); ///< return the hostname of the IP address
  static std::string getHostByAddr(int ipaddr); ///< equivalent to getHostname(int)
  static std::string getAddrString(int ipaddr); ///< returns the IP address as a string
  static std::string getAddrString(const std::string& hostname) throw (AddressException); ///< returns the IP address as a string
  /**
   * Address string format is one of
   * - IP
   * - IP:port
   * - IP:port/IP:port
   * - (NAT):id
   * - (NAT):id/IP:port
   */
  static std::string getAddrString(const MaceAddr& addr, bool resolve = true); ///< prints the address string of the MaceAddr, optionally use DNS
  /**
   * Address string format is one of
   * - IP
   * - IP:port
   * - IP:port/IP:port
   * - (NAT):id
   * - (NAT):id/IP:port
   */
  static std::string getAddrString(const SockAddr& addr, bool resolve = true); ///< prints the address string of the SockAddr, optionally use DNS
  /**
   * Address string format is one of
   * - IP
   * - IP:port
   * - IP:port/IP:port
   * - (NAT):id
   * - (NAT):id/IP:port
   */
  static void printAddrString(std::ostream& out, const MaceAddr& addr, bool resolve = true); ///< prints the address string to an ostream optionally using DNS
  /**
   * Address string format is one of
   * - IP
   * - IP:port
   * - IP:port/IP:port
   * - (NAT):id
   * - (NAT):id/IP:port
   */
  static void printAddrString(std::ostream& out, const SockAddr& addr, bool resolve = true); ///< prints the address string to an ostream optionally using DNS
  /**
   * Address string format is one of
   * - IP
   * - IP:port
   * - IP:port/IP:port
   * - (NAT):id
   * - (NAT):id/IP:port
   */
  static void printAddrString(std::ostream& out, const std::string& hostname) throw (AddressException); ///< prints the address string to an ostream optionally using DNS
  /**
   * Address string format is one of
   * - IP
   * - IP:port
   * - IP:port/IP:port
   * - (NAT):id
   * - (NAT):id/IP:port
   */
  static void printAddrString(std::ostream& out, int ipaddr); ///< prints the address string to an ostream optionally using DNS

  static std::string getErrorString(int err); ///< return an error string for an error code (a la strerror())
  static std::string getSslErrorString(); ///< return the SSL last error string

  static mace::map<int, int> makeMap(int first ...);

  static void nodeSetDiff(const NodeSet& prev, const NodeSet& cur,
			  NodeSet& added, NodeSet& removed);

private:
  static const size_t DNS_CACHE_TIMEOUT = 10 * 60;
  static const unsigned DNS_CACHE_SIZE = 64;
  static uint16_t baseport;
};

/** @} */

#endif // __UTIL_H


text:
/* Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 *      http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 */
package org.camunda.bpm.engine.impl.cmmn.execution;

import java.util.List;

import org.camunda.bpm.engine.ProcessEngineException;
import org.camunda.bpm.engine.delegate.DelegateCaseExecution;
import org.camunda.bpm.engine.exception.cmmn.CaseIllegalStateTransitionException;
import org.camunda.bpm.engine.impl.cmmn.model.CmmnActivity;
import org.camunda.bpm.engine.impl.cmmn.model.CmmnCaseDefinition;
import org.camunda.bpm.engine.impl.pvm.PvmProcessDefinition;
import org.camunda.bpm.engine.impl.pvm.PvmProcessInstance;
import org.camunda.bpm.engine.impl.task.TaskDecorator;
import org.camunda.bpm.engine.runtime.CaseInstance;
import org.camunda.bpm.engine.runtime.ProcessInstance;
import org.camunda.bpm.model.cmmn.instance.CaseTask;
import org.camunda.bpm.model.cmmn.instance.EventListener;
import org.camunda.bpm.model.cmmn.instance.HumanTask;
import org.camunda.bpm.model.cmmn.instance.IfPart;
import org.camunda.bpm.model.cmmn.instance.Milestone;
import org.camunda.bpm.model.cmmn.instance.PlanItemOnPart;
import org.camunda.bpm.model.cmmn.instance.ProcessTask;
import org.camunda.bpm.model.cmmn.instance.Sentry;
import org.camunda.bpm.model.cmmn.instance.Stage;
import org.camunda.bpm.model.cmmn.instance.Task;
import org.camunda.bpm.model.cmmn.instance.UserEventListener;

/**
 * @author Roman Smirnov
 *
 */
public interface CmmnActivityExecution extends DelegateCaseExecution {

  /**
   *
Returns the parent of this case execution, or null
   * if there is no parent.

   * @return a {@link CmmnActivityExecution parent} or null.
   */
  CmmnActivityExecution getParent();

  /**
   *
Returns true if this case execution
   * is a case instance. If this case execution is not a
   * case instance then false will be returned.

   *
   * @return whether this case execution is a case instance or not.
   */
  boolean isCaseInstanceExecution();

  /**
   *
Returns the {@link CaseExecutionState current state} of this
   * case execution.

   *
   * @return the {@link CaseExecutionState current state}
   */
  CaseExecutionState getCurrentState();

  /**
   *
Sets the given {@link CaseExecutionState state} as the
   * current state of this case execution.

   *
   * @param currentState the current state to set
   */
  void setCurrentState(CaseExecutionState currentState);

  /**
   *
Returns the {@link CaseExecutionState previous state} of this
   * case execution.

   *
   * @return the {@link CaseExecutionState previous state}
   */
  CaseExecutionState getPreviousState();

  /**
   *
Returns true iff:

   *  {@link #getCurrentState()} == {@link CaseExecutionState#NEW}
   *

   *
   * @return whether this case execution has as current state {@link CaseExecutionState#NEW}
   */
  boolean isNew();

  /**
   *
Returns true iff:

   *  {@link #getCurrentState()} == {@link CaseExecutionState#TERMINATING_ON_TERMINATION}
   *        || {@link #getCurrentState()} == {@link CaseExecutionState#TERMINATING_ON_PARENT_TERMINATION}
   *        || {@link #getCurrentState()} == {@link CaseExecutionState#TERMINATING_ON_EXIT}
   *

   *
   * @return whether this case execution has as current state {@link CaseExecutionState#TERMINATING_ON_TERMINATION},
   *         {@link CaseExecutionState#TERMINATING_ON_PARENT_TERMINATION} or {@link CaseExecutionState#TERMINATING_ON_EXIT}
   */
  boolean isTerminating();

  /**
   *
Returns true iff:

   *  {@link #getCurrentState()} == {@link CaseExecutionState#SUSPENDING_ON_SUSPENSION}
   *        || {@link #getCurrentState()} == {@link CaseExecutionState#SUSPENDING_ON_PARENT_SUSPENSION}
   *

   *
   * @return whether this case execution has as current state
   *        {@link CaseExecutionState#SUSPENDING_ON_SUSPENSION} or {@link CaseExecutionState#SUSPENDING_ON_PARENT_SUSPENSION}
   */
  boolean isSuspending();

  /**
   *
Returns the {@link CmmnActivity activity} which is associated with
   * this case execution.
   *
   * @return the associated {@link CmmnActivity activity}
   */
  CmmnActivity getActivity();

  /**
   *
Creates new child case executions for each given {@link CmmnActivity}.

   *
   *
Afterwards the method {@link #triggerChildExecutionsLifecycle(List)} must be called
   * to execute each created case executions (ie. the create listener will be
   * notified etc.).

   *
   *
According to the CMMN 1.0 specification:

   * This method can be called when this case execution (which
   * represents a {@link Stage}) transitions to ACTIVE state.
   * The passed collection of {@link CmmnActivity activities} are the planned
   * items that should be executed in this {@link Stage}. So that for each
   * given {@link CmmnActivity} a new case execution will be instantiated.
   * Furthermore for each created child execution there happens a transition
   * to the initial state AVAILABLE.
   *

   *
   * @param activities a collection of {@link CmmnActivity activities} of planned items
   *                   to execute inside this case execution
   */
  List<CmmnExecution> createChildExecutions(List<CmmnActivity> activities);

  /**
   *
This method triggers for each given case execution the lifecycle.

   *
   *
This method must be called after {@link #createChildExecutions(List)}.

   *
   * @param children a collection of {@link CmmnExecution case execution} to
   *                 trigger for each given case execution the lifecycle
   */
  void triggerChildExecutionsLifecycle(List<CmmnExecution> children);

  /**
   *
Transition to {@link CaseExecutionState#ENABLED} state.

   *
   *
This case execution must be in {@link CaseExecutionState#AVAILABLE}
   * state to be able to do this transition.

   *
   *
It is only possible to enable a case execution which is associated with a
   * {@link Stage} or {@link Task}.

   *
   * @throws CaseIllegalStateTransitionException will be thrown, if this case execution
   *         is not {@link CaseExecutionState#AVAILABLE}.
   * @throws ProcessEngineException when an internal exception happens during the execution
   *     of the command.
   */
  void enable();

  /**
   *
Transition to  state.

   *
   *
This case execution must be in {@link CaseExecutionState#ENABLED}
   * state to be able to do this transition.

   *
   *
It is only possible to disable a case execution which is associated with a
   * {@link Stage} or {@link Task}.

   *
   *
If this case execution has a parent case execution, that parent
   * case execution will be notified that this case execution has been
   * disabled. This can lead to a completion of the parent case execution, for more
   * details when the parent case execution can be completed see {@link #complete()}.

   *
   * @throws CaseIllegalStateTransitionException will be thrown, if this case execution
   *         is not {@link CaseExecutionState#ENABLED}.
   * @throws ProcessEngineException when an internal exception happens during the execution
   *     of the command.
   */
  void disable();

  /**
   *
Transition to {@link CaseExecutionState#ENABLED} state.

   *
   *
This case execution must be in {@link CaseExecutionState#DISABLED}
   * state to be able to do this transition.

   *
   *
It is only possible to re-enable a case execution which is associated with a
   * {@link Stage} or {@link Task}.

   *
   * @throws CaseIllegalStateTransitionException will be thrown, if this case execution
   *         is not {@link CaseExecutionState#DISABLED}.
   * @throws ProcessEngineException when an internal exception happens during the execution
   *     of the command.
   */
  void reenable();

  /**
   *
Transition to {@link CaseExecutionState#ACTIVE} state.

   *
   *
This case execution must be in {@link CaseExecutionState#ENABLED}
   * state to be able to do this transition.

   *
   *
It is only possible to start a case execution manually which is associated with a
   * {@link Stage} or {@link Task}.

   *
   * @throws CaseIllegalStateTransitionException will be thrown, if this case execution
   *         is not {@link CaseExecutionState#ENABLED}.
   * @throws ProcessEngineException when an internal exception happens during the execution
   *     of the command.
   */
  void manualStart();

  /**
   *
Transition to {@link CaseExecutionState#ACTIVE} state.

   *
   *
This case execution must be in {@link CaseExecutionState#AVAILABLE}
   * state to be able to do this transition.

   *
   *
It is only possible to start a case execution which is associated with a
   * {@link Stage} or {@link Task}.

   *
   * @throws CaseIllegalStateTransitionException will be thrown, if this case execution
   *         is not {@link CaseExecutionState#AVAILABLE}.
   * @throws ProcessEngineException when an internal exception happens during the execution
   *     of the command.
   */
  void start();

  /**
   *
Transition to {@link CaseExecutionState#COMPLETED} state.

   *
   *
This case execution must be in {@link CaseExecutionState#ACTIVE}
   * state to be able to do this transition.

   *
   *
It is only possible to complete a case execution which is associated with a
   * {@link Stage} or {@link Task}.

   *
   *
If this case execution has a parent case execution, that parent
   * case execution will be notified that this case execution has been
   * completed. This can lead to a completion of the parent case execution, for more
   * details when the parent case execution can be completed see {@link #complete()}.

   *
   *
In case of a {@link Stage} the completion can only be performed when the following
   * criteria are fulfilled:

   *

   *
there are no children in the state {@link CaseExecutionState#ACTIVE} or {@link CaseExecutionState#NEW}

   *
if the property autoComplete of the associated {@link Stage} is set to true:
   *

   *
all required (requiredRule evaluates to true) children are in state
   *

   *
{@link CaseExecutionState#DISABLED}

   *
{@link CaseExecutionState#COMPLETED}

   *
{@link CaseExecutionState#TERMINATED}

   *
{@link CaseExecutionState#FAILED}

   *

   *

   *

   *

   *
if the property autoComplete of the associated {@link Stage} is set to false:
   *

   *
all children are in
   *

   *
{@link CaseExecutionState#DISABLED}

   *
{@link CaseExecutionState#COMPLETED}

   *
{@link CaseExecutionState#TERMINATED}

   *
{@link CaseExecutionState#FAILED}

   *

   *

   *

   *

   *

   *

   *
   *
For a {@link Task} instance, this means its purpose has been accomplished:

   *

   *
{@link HumanTask} have been completed by human.

   *
{@link CaseTask} have launched a new {@link CaseInstance} and if output parameters
   *        are required and/or the property isBlocking is set to true,
   *        then the launched {@link CaseInstance} has completed and returned the
   *        output parameters.

   *
{@link ProcessTask} have launched a new {@link ProcessInstance} and if output parameters
   *        are required and/or the property isBlocking is set to true,
   *        then the launched {@link ProcessInstance} has completed and returned the
   *        output parameters.

   *

   *

   *
   * @throws CaseIllegalStateTransitionException will be thrown, if this case execution
   *         is not {@link CaseExecutionState#ACTIVE} or when the case execution cannot be
   *         completed.
   * @throws ProcessEngineException when an internal exception happens during the execution
   *     of the command.
   */
  void complete();

  /**
   *
Transition to {@link CaseExecutionState#COMPLETED} state.

   *
   *
This case execution must be in {@link CaseExecutionState#ACTIVE}
   * state to be able to do this transition.

   *
   *
It is only possible to complete a case execution manually which is associated with a
   * {@link Stage} or {@link Task}.

   *
   *
If this case execution has a parent case execution, that parent
   * case execution will be notified that this case execution has been
   * completed. This can lead to a completion of the parent case execution, for more
   * details when the parent case execution can be completed see {@link #complete()}.

   *
   *
In case of a {@link Stage} the completion can only be performed when the following
   * criteria are fulfilled:

   *

   *
there are no children in the state {@link CaseExecutionState#ACTIVE} or {@link CaseExecutionState#NEW}

   *
all required (requiredRule evaluates to true) children are in state
   *

   *
{@link CaseExecutionState#DISABLED}

   *
{@link CaseExecutionState#COMPLETED}

   *
{@link CaseExecutionState#TERMINATED}

   *
{@link CaseExecutionState#FAILED}

   *

   *

   *

   *

   *
   *
For a {@link Task} instance, this means its purpose has been accomplished:

   *

   *
{@link HumanTask} have been completed by human.

   *

   *

   *
   * @throws CaseIllegalStateTransitionException will be thrown, if this case execution
   *         is not {@link CaseExecutionState#ACTIVE} or when the case execution cannot be
   *         completed.
   * @throws ProcessEngineException when an internal exception happens during the execution
   *     of the command.
   */
  void manualComplete();

  /**
   *
Transition to {@link CaseExecutionState#COMPLETED} state.

   *
   *
This case execution must be in {@link CaseExecutionState#AVAILABLE}
   * state to be able to do this transition.

   *
   *
For {@link EventListener event listener} transitions when the event being listened by the
   * {@link EventListener event listener} instance does occur. For a {@link UserEventListener user event
   * listener} instance this transition happens when a human decides to raise the event.

   *
   *
For {@link Milestone} instance transitions when one of the achieving {@link Sentry sentries}
   * (entry criteria) is satisfied.

   *
   *
If this case execution has a parent case execution, that parent
   * case execution will be notified that this case execution has been
   * completed (ie.the event or milestone occured). This can lead to a completion of
   * the parent case execution, for more details when the parent case execution can
   * be completed see {@link #complete()}.

   *
   * @throws CaseIllegalStateTransitionException will be thrown, if this case execution
   *         is not {@link CaseExecutionState#AVAILABLE}.
   * @throws ProcessEngineException when an internal exception happens during the execution
   *     of the command.
   */
  void occur();

  /**
   *
Transition to {@link CaseExecutionState#TERMINATING_ON_TERMINATION} state.

   *
   *
If this case execution is associated with a {@link Stage} or
   * {@link Task}, then this case execution must be in {@link CaseExecutionState#ACTIVE}
   * state to be able to do this transition.

   * And if this case execution is association with {@link EventListener EventListener}
   * or a {@link Milestone}, then this case execution must be in
   * {@link CaseExecutionState#AVAILABLE} state to be able to do this transition.

   *
   *
For a {@link Stage} instance the termination of this case execution
   * will be propagated down to all its contained {@link EventListener EventListener}, {@link Milestone},
   * {@link Stage}, and {@link Task} instances.

   *
   *
In case of a {@link Stage} this corresponding case execution stays in this state until
   * all children notified this case execution, that they terminated successfully. Afterwards the
   * method {@link #performTerminate()} must be called to complete the transition into the state
   * {@link CaseExecutionState#TERMINATED}.

   *
   * @throws CaseIllegalStateTransitionException will be thrown, if this case execution
   *         is not in the expected state.
   * @throws ProcessEngineException when an internal exception happens during the execution
   *     of the command.
   */
  void terminate();

  /**
   *
Transition to {@link CaseExecutionState#TERMINATED} state.

   *
   *
If this case execution has a parent case execution, that parent
   * case execution will be notified that this case execution has been
   * terminated. This can lead to a completion of the parent case execution, for more
   * details when the parent case execution can be completed see {@link #complete()}.

   *
   * @throws CaseIllegalStateTransitionException will be thrown, if this case execution
   *         is not in the expected state.
   * @throws ProcessEngineException when an internal exception happens during the execution
   *     of the command.
   */
  void performTerminate();

  /**
   *
Transition to {@link CaseExecutionState#TERMINATING_ON_PARENT_TERMINATION} state.

   *
   *
This case execution must be in {@link CaseExecutionState#AVAILABLE}
   * or {@link CaseExecutionState#SUSPENDED} state to be able to do this transition.

   *
   *
It is only possible to execute a parent termination on a case execution which is
   * associated with a {@link EventListener} or {@link Milestone}.

   *
   *
Afterwards the method {@link #performParentTerminate()} must be called to complete
   * the transition into the state {@link CaseExecutionState#TERMINATED}.

   *
   * @throws CaseIllegalStateTransitionException will be thrown, if this case execution
   *         is not in the expected state.
   * @throws ProcessEngineException when an internal exception happens during the execution
   *     of the command.
   */
  void parentTerminate();

  /**
   *
Transition to {@link CaseExecutionState#TERMINATED} state.

   *
   *
This case execution must be in {@link CaseExecutionState#AVAILABLE}
   * or {@link CaseExecutionState#SUSPENDED} state to be able to do this transition.

   *
   *
It is only possible to execute a parent termination on a case execution which is
   * associated with a {@link EventListener} or {@link Milestone}.

   *
   * @throws CaseIllegalStateTransitionException will be thrown, if this case execution
   *         is not in the expected state.
   * @throws ProcessEngineException when an internal exception happens during the execution
   *     of the command.
   */
  void performParentTerminate();

  /**
   *
Transition to {@link CaseExecutionState#TERMINATING_ON_EXIT} state.

   *
   *
This case execution must be in one of the following state to
   * be able to do this transition:
   *

   *
{@link CaseExecutionState#AVAILABLE},

   *
{@link CaseExecutionState#ENABLED},

   *
{@link CaseExecutionState#DISABLED},

   *
{@link CaseExecutionState#ACTIVE},

   *
{@link CaseExecutionState#SUSPENDED} or

   *
{@link CaseExecutionState#FAILED}

   *

   *
   *
It is only possible to execute an exit on a case execution which is
   * associated with a {@link Stage} or {@link Task}.

   *
   *
Afterwards the method {@link #performExit()} must be called to complete
   * the transition into the state {@link CaseExecutionState#TERMINATED}.

   *
   *
If this transition is triggered by a fulfilled exit criteria and if
   * this case execution has a parent case execution, that parent
   * case execution will be notified that this case execution has been
   * terminated. This can lead to a completion of the parent case execution, for more
   * details when the parent case execution can be completed see {@link #complete()}.

   *
   * @throws CaseIllegalStateTransitionException will be thrown, if this case execution
   *         is not in the expected state.
   * @throws ProcessEngineException when an internal exception happens during the execution
   *     of the command.
   */
  void exit();

  /**
   *
Transition to {@link CaseExecutionState#TERMINATED} state.

   *
   *
This can lead to a completion of the parent case execution, for more
   * details when the parent case execution can be completed see {@link #complete()}.

   *
   * @throws CaseIllegalStateTransitionException will be thrown, if this case execution
   *         is not in the expected state.
   * @throws ProcessEngineException when an internal exception happens during the execution
   *     of the command.
   */
  void performExit();

  /**
   *
Transition to {@link CaseExecutionState#SUSPENDING_ON_SUSPENSION} state.

   *
   *
If this case execution is associated with a {@link Stage} or
   * {@link Task}, then this case execution must be in {@link CaseExecutionState#ACTIVE}
   * state to be able to do this transition.

   * And if this case execution is association with {@link EventListener EventListener}
   * or a {@link Milestone}, then this case execution must be in
   * {@link CaseExecutionState#AVAILABLE} state to be able to do this transition.

   *
   *
For a {@link Stage} instance the suspension of this case execution
   * will be propagated down to all its contained {@link EventListener EventListener}, {@link Milestone},
   * {@link Stage}, and {@link Task} instances.

   *
   *
Afterwards the method {@link #performSuspension()} must be called to complete
   * the transition into the state {@link CaseExecutionState#SUSPENDED}.

   *
   * @throws CaseIllegalStateTransitionException will be thrown, if this case execution
   *         is not in the expected state.
   * @throws ProcessEngineException when an internal exception happens during the execution
   *     of the command.
   */
  void suspend();

  /**
   *
Transition to {@link CaseExecutionState#SUSPENDED} state.

   *
   * @throws CaseIllegalStateTransitionException will be thrown, if this case execution
   *         is not in the expected state.
   * @throws ProcessEngineException when an internal exception happens during the execution
   *     of the command.
   */
  void performSuspension();

  /**
   *
Transition to {@link CaseExecutionState#SUSPENDING_ON_PARENT_SUSPENSION} state.

   *
   *
This case execution must be in one of the following state to
   * be able to do this transition:
   *

   *
{@link CaseExecutionState#AVAILABLE},

   *
{@link CaseExecutionState#ENABLED},

   *
{@link CaseExecutionState#DISABLED} or

   *
{@link CaseExecutionState#ACTIVE}

   *

   *
   *
It is only possible to execute a parent suspension on a case execution which is
   * associated with a {@link Stage} or {@link Task}.

   *
   *
Afterwards the method {@link #performParentSuspension()} must be called to complete
   * the transition into the state {@link CaseExecutionState#SUSPENDED}.

   *
   * @throws CaseIllegalStateTransitionException will be thrown, if this case execution
   *         is not in the expected state.
   * @throws ProcessEngineException when an internal exception happens during the execution
   *     of the command.
   */
  void parentSuspend();

  /**
   *
Transition to {@link CaseExecutionState#SUSPENDED} state.

   *
   * @throws CaseIllegalStateTransitionException will be thrown, if this case execution
   *         is not in the expected state.
   * @throws ProcessEngineException when an internal exception happens during the execution
   *     of the command.
   */
  void performParentSuspension();

  /**
   *
Transition to either to {@link CaseExecutionState#ACTIVE} state, if this
   * case execution is associated with a {@link Stage} or {@link Task}, or to {@link CaseExecutionState#AVAILABE},
   * if this case execution is associated with a {@link EventListener} or {@link Milestone}.

   *
   *
This case execution must be in {@link CaseExecutionState#SUSPENDED}
   * state to be able to do this transition.

   *
   *
For a {@link Stage} instance the resume of this case execution
   * will be propagated down to all its contained {@link EventListener EventListener}, {@link Milestone},
   * {@link Stage}, and {@link Task} instances.

   *
   * @throws CaseIllegalStateTransitionException will be thrown, if this case execution
   *         is not in the expected state.
   * @throws ProcessEngineException when an internal exception happens during the execution
   *     of the command.
   */
  void resume();

  /**
   *
Transition to the previous state ({@link CaseExecutionState#AVAILABLE},
   * {@link CaseExecutionState#ENABLED}, {@link CaseExecutionState#DISABLED} or
   * {@link CaseExecutionState#ACTIVE}) when the parent {@link Stage} transitions
   * out of {@link CaseExecutionState#SUSPENDED}.

   *
   *
This case execution must be in {@link CaseExecutionState#SUSPENDED}
   * state to be able to do this transition.

   *
   *
It is only possible to execute a parent resume on a case execution which is
   * associated with a {@link Stage} or {@link Task}.

   *
   * @throws CaseIllegalStateTransitionException will be thrown, if this case execution
   *         is not in the expected state.
   * @throws ProcessEngineException when an internal exception happens during the execution
   *     of the command.
   */
  void parentResume();

  /**
   *
Transition to {@link CaseExecutionState#ACTIVE} state.

   *
   *
If this case execution is associated with a {@link Stage} or
   * {@link Task} and is not a case instance, then this case execution
   * must be in {@link CaseExecutionState#FAILED} state to be able to do this transition.

   * And if this case execution is a case instance, then this
   * case instance must be in one of the following state to perform this transition:
   *

   *
{@link CaseExecutionState#COMPLETED},

   *
{@link CaseExecutionState#SUSPENDED},

   *
{@link CaseExecutionState#TERMINATED} or

   *
{@link CaseExecutionState#FAILED}

   *

   *

   *
   *
In case of a case instance the transition out of {@link CaseExecutionState#SUSPENDED} state
   * the resume will be propagated down to all its contained {@link EventListener EventListener},
   * {@link Milestone}, {@link Stage}, and {@link Task} instances, see {@link #resume()} and
   * {@link #parentResume()}.

   *
   * @throws CaseIllegalStateTransitionException will be thrown, if this case execution
   *         is not in the expected state.
   * @throws ProcessEngineException when an internal exception happens during the execution
   *     of the command.
   */
  void reactivate();

  /**
   *
Transition to {@link CaseExecutionState#CLOSED} state when no further
   * work or modifications should be allowed for this case instance.

   *
   *
It is only possible to close a case instance which is in one of the following
   * states:
   *

   *
{@link CaseExecutionState#COMPLETED},

   *
{@link CaseExecutionState#SUSPENDED},

   *
{@link CaseExecutionState#TERMINATED} or

   *
{@link CaseExecutionState#FAILED}

   *

   *

   *
   * @throws CaseIllegalStateTransitionException will be thrown, if this case execution
   *         is not in the expected state.
   * @throws ProcessEngineException when an internal exception happens during the execution
   *     of the command.
   */
  void close();

  /**
   *
Returns to true, if this case execution is required.

   *
   * @return true if this case execution is required.
   */
  boolean isRequired();

  /**
   *
Sets this case execution as required or not required.

   *
   * @param required a boolean value whether this case execution
   * is required or not required.
   */
  void setRequired(boolean required);

  /**
   *
Removes this case execution from the parent case execution.

   */
  void remove();

  /**
   *
Returns a {@link List} of child case executions. If this case
   * execution has no child case executions an empty {@link List} will be returned.

   *
   * @return a {@link List} of child case executions.
   */
  List<? extends CmmnExecution> getCaseExecutions();

  /**
   *
Creates a new task.

   *
   *
This
 case execution will be the case execution of the
   * created task.

   *
   * @param taskDecorator the task decorator used to create task
   */
   org.camunda.bpm.engine.task.Task createTask(TaskDecorator taskDecorator);

  /**
   *
Creates a new sub process instance.

   *
   *
This case execution will be the super case execution of the
   * created sub process instance.

   *
   * @param processDefinition The {@link PvmProcessDefinition} of the subprocess.
   */
  PvmProcessInstance createSubProcessInstance(PvmProcessDefinition processDefinition);

  /**
   *
Creates a new sub process instance.

   *
   *
This case execution will be the super case execution of the
   * created sub process instance.

   *
   * @param processDefinition The {@link PvmProcessDefinition} of the subprocess.
   * @param businessKey The businessKey to be set on sub process instance.
   */
  PvmProcessInstance createSubProcessInstance(PvmProcessDefinition processDefinition, String businessKey);

  /**
   *
Creates a new sub process instance.

   *
   *
This case execution will be the super case execution of the
   * created sub process instance.

   *
   * @param processDefinition The {@link PvmProcessDefinition} of the subprocess.
   * @param businessKey The businessKey to be set on sub process instance.
   * @param caseInstanceId The caseInstanceId to be set on sub process instance.
   */
  PvmProcessInstance createSubProcessInstance(PvmProcessDefinition processDefinition, String businessKey, String caseInstanceId);

  /**
   *
Creates a new sub case instance.

   *
   *
This case execution will be the super case execution of the
   * created sub case instance.

   *
   * @param caseDefinition The {@link CmmnCaseDefinition} of the sub case instance.
   */
  CmmnCaseInstance createSubCaseInstance(CmmnCaseDefinition caseDefinition);

  /**
   *
Creates a new sub case instance.

   *
   *
This case execution will be the super case execution of the
   * created sub case instance.

   *
   * @param caseDefinition The {@link CmmnCaseDefinition} of the sub case instance.
   * @param businessKey The businessKey to be set on sub case instance.
   */
  CmmnCaseInstance createSubCaseInstance(CmmnCaseDefinition caseDefinition, String businessKey);

  /**
   *
Creates for each defined {@link PlanItemOnPart} and {@link IfPart} inside
   * the specified {@link Sentry Sentries} a {@link CmmnSentryPart}.

   */
  void createSentryParts();

  /**
   *
Returns true, if each {@link CmmnSentryPart} of the given
   * sentryId is satisfied.
   *
   * @param sentryId the id of the sentry to check
   *
   * @return true if the sentry is satisfied.
   */
  boolean isSentrySatisfied(String sentryId);
}


text:
namespace gin {

class ModuleRegistryObserver;
struct PendingModule;

// This class implements the Asynchronous Module Definition (AMD) API.
// https://github.com/amdjs/amdjs-api/wiki/AMD
//
// Our implementation isn't complete yet. Missing features:
//   1) Built-in support for require, exports, and module.
//   2) Path resoltuion in module names.
//
// For these reasons, we don't have an "amd" property on the "define"
// function. The spec says we should only add that property once our
// implementation complies with the specification.
//
class GIN_EXPORT ModuleRegistry {
 public:
  typedef base::Callback<void (v8::Handle<v8::Value>)> LoadModuleCallback;

  virtual ~ModuleRegistry();

  static ModuleRegistry* From(v8::Handle<v8::Context> context);

  static void RegisterGlobals(v8::Isolate* isolate,
                              v8::Handle<v8::ObjectTemplate> templ);

  // Installs the necessary functions needed for modules.
  // WARNING: this may execute script in the page.
  static void InstallGlobals(v8::Isolate* isolate, v8::Handle<v8::Object> obj);

  void AddObserver(ModuleRegistryObserver* observer);
  void RemoveObserver(ModuleRegistryObserver* observer);

  // The caller must have already entered our context.
  void AddBuiltinModule(v8::Isolate* isolate, const std::string& id,
                        v8::Handle<v8::Value> module);

  // The caller must have already entered our context.
  void AddPendingModule(v8::Isolate* isolate,
                        scoped_ptr<PendingModule> pending);

  void LoadModule(v8::Isolate* isolate,
                  const std::string& id,
                  LoadModuleCallback callback);

  // The caller must have already entered our context.
  void AttemptToLoadMoreModules(v8::Isolate* isolate);

  const std::set<std::string>& available_modules() const {
    return available_modules_;
  }

  const std::set<std::string>& unsatisfied_dependencies() const {
    return unsatisfied_dependencies_;
  }

 private:
  typedef ScopedVector<PendingModule> PendingModuleVector;
  typedef std::multimap<std::string, LoadModuleCallback> LoadModuleCallbackMap;

  explicit ModuleRegistry(v8::Isolate* isolate);

  void Load(v8::Isolate* isolate, scoped_ptr<PendingModule> pending);
  void RegisterModule(v8::Isolate* isolate,
                      const std::string& id,
                      v8::Handle<v8::Value> module);

  bool CheckDependencies(PendingModule* pending);
  bool AttemptToLoad(v8::Isolate* isolate, scoped_ptr<PendingModule> pending);

  v8::Handle<v8::Value> GetModule(v8::Isolate* isolate, const std::string& id);

  std::set<std::string> available_modules_;
  std::set<std::string> unsatisfied_dependencies_;

  LoadModuleCallbackMap waiting_callbacks_;

  PendingModuleVector pending_modules_;
  v8::Persistent<v8::Object> modules_;

  ObserverList<ModuleRegistryObserver> observer_list_;

  DISALLOW_COPY_AND_ASSIGN(ModuleRegistry);
};

}  // namespace gin

#endif  // GIN_MODULES_MODULE_REGISTRY_H_