Moved more of the checkInitVar tests to the new system
This commit is contained in:
Neil Brown
parent
810c798dac
commit
3b57d43eb6
|
|
@ -184,69 +184,37 @@ testInitVar = TestList
|
|||
,oX *:= oZ
|
||||
]
|
||||
]]]
|
||||
|
||||
-- Single node, x not touched
|
||||
,testInitVarPass 0 [(0,[],[])] [] 0 0 "x"
|
||||
-- Single node, x written to
|
||||
,testInitVarPass 1 [(0,[],[variable "x"])] [] 0 0 "x"
|
||||
-- Single node, x read from (FAIL)
|
||||
,testInitVarFail 2 [(0,[variable "x"],[])] [] 0 0 "x"
|
||||
-- Single node, x read from and written to (FAIL - x must be written to before the read.
|
||||
-- This line is akin to x = x + 1, so x must be written to beforehand)
|
||||
,testInitVarFail 3 [(0,[variable "x"],[variable "x"])] [] 0 0 "x"
|
||||
|
||||
-- Two nodes, x written to then read
|
||||
,testInitVarPass 10 [(0,[],[variable "x"]), (1,[variable "x"],[])] [(0,1,ESeq Nothing)] 0 1 "x"
|
||||
-- Two nodes, x read then written to (FAIL)
|
||||
,testInitVarFail 11 [(0,[],[variable "x"]), (1,[variable "x"],[])] [(1,0,ESeq Nothing)] 1 0 "x"
|
||||
-- As test 10 (x written to then read) but using the par edges.
|
||||
,testInitVarPass 13 [(0,[],[variable "x"]), (1,[variable "x"],[])] [(0,1,EStartPar 0)] 0 1 "x"
|
||||
,testInitVarPass 14 [(0,[],[variable "x"]), (1,[variable "x"],[])] [(0,1,EEndPar 0)] 0 1 "x"
|
||||
|
||||
-- Diamond tests (0 branches to 1 and 2, which both merge to 3):
|
||||
-- x written to in 0 and 1, then read in 3
|
||||
,testInitVarPass 20 [(0,[],[]),(1,[],[variable "x"]), (2,[],[variable "x"]), (3,[variable "x"],[])]
|
||||
[(0,1,ESeq Nothing),(0,2,ESeq Nothing),(1,3,ESeq Nothing),(2,3,ESeq Nothing)] 0 3 "x"
|
||||
-- x written to only in 2 then read in 3 (FAIL)
|
||||
,testInitVarFail 21 [(0,[],[]),(1,[],[]), (2,[],[variable "x"]), (3,[variable "x"],[])]
|
||||
[(0,1,ESeq Nothing),(0,2,ESeq Nothing),(1,3,ESeq Nothing),(2,3,ESeq Nothing)] 0 3 "x"
|
||||
-- x definitely written to in 2, but not 1 (FAIL)
|
||||
,testInitVarFail 22 [(0,[],[]),(1,[],[]), (2,[],[variable "x"]), (3,[variable "x"],[])]
|
||||
[(0,1,ESeq Nothing),(0,2,ESeq Nothing),(1,3,ESeq Nothing),(2,3,ESeq Nothing)] 0 3 "x"
|
||||
-- like test 21, but the link missing from 1 to 3, so test will pass
|
||||
,testInitVarPass 23 [(0,[],[]),(1,[],[]), (2,[],[variable "x"]), (3,[variable "x"],[])]
|
||||
[(0,1,ESeq Nothing),(0,2,ESeq Nothing),(2,3,ESeq Nothing)] 0 3 "x"
|
||||
-- variable written to in 0, read in 3
|
||||
,testInitVarPass 24 [(0,[],[variable "x"]),(1,[],[]), (2,[],[]), (3,[variable "x"],[])]
|
||||
[(0,1,ESeq Nothing),(0,2,ESeq Nothing),(1,3,ESeq Nothing),(2,3,ESeq Nothing)] 0 3 "x"
|
||||
-- variable never written to, but read in 3
|
||||
,testInitVarFail 25 [(0,[],[]),(1,[],[]), (2,[],[]), (3,[variable "x"],[])]
|
||||
[(0,1,ESeq Nothing),(0,2,ESeq Nothing),(1,3,ESeq Nothing),(2,3,ESeq Nothing)] 0 3 "x"
|
||||
-- variable written to in 2 and 3, but read in 1 (FAIL):
|
||||
,testInitVarFail 26 [(0,[],[]),(1,[variable "x"],[]), (2,[],[variable "x"]), (3,[],[variable "x"])]
|
||||
[(0,1,ESeq Nothing),(0,2,ESeq Nothing),(1,3,ESeq Nothing),(2,3,ESeq Nothing)] 0 3 "x"
|
||||
|
||||
-- Test parallel diamonds:
|
||||
-- written to in 1 and 2, read in 3
|
||||
-- This would fail CREW, but that's not what we're testing here:
|
||||
,testInitVarPass 30 [(0,[],[]),(1,[],[variable "x"]), (2,[],[variable "x"]), (3,[variable "x"],[])]
|
||||
[(0,1,EStartPar 0),(0,2,EStartPar 0),(1,3,EEndPar 0),(2,3,EEndPar 0)] 0 3 "x"
|
||||
-- written to in 1, read in 3
|
||||
,testInitVarPass 31 [(0,[],[]),(1,[],[variable "x"]), (2,[],[]), (3,[variable "x"],[])]
|
||||
[(0,1,EStartPar 0),(0,2,EStartPar 0),(1,3,EEndPar 0),(2,3,EEndPar 0)] 0 3 "x"
|
||||
-- written to in 0, read in 3
|
||||
,testInitVarPass 32 [(0,[],[variable "x"]),(1,[],[]), (2,[],[]), (3,[variable "x"],[])]
|
||||
[(0,1,EStartPar 0),(0,2,EStartPar 0),(1,3,EEndPar 0),(2,3,EEndPar 0)] 0 3 "x"
|
||||
-- never written to, but read in 3:
|
||||
,testInitVarFail 33 [(0,[],[]),(1,[],[]), (2,[],[]), (3,[variable "x"],[])]
|
||||
[(0,1,EStartPar 0),(0,2,EStartPar 0),(1,3,EEndPar 0),(2,3,EEndPar 0)] 0 3 "x"
|
||||
-- written to in 1, read in 2 (again, would fail CREW) (FAIL):
|
||||
,testInitVarFail 34 [(0,[],[]),(1,[],[variable "x"]), (2,[variable "x"],[]), (3,[],[])]
|
||||
[(0,1,EStartPar 0),(0,2,EStartPar 0),(1,3,EEndPar 0),(2,3,EEndPar 0)] 0 3 "x"
|
||||
-- written to in 1, read in 2 and 3 (again, would fail CREW) (FAIL):
|
||||
,testInitVarFail 35 [(0,[],[]),(1,[],[variable "x"]), (2,[variable "x"],[]), (3,[variable "x"],[])]
|
||||
[(0,1,EStartPar 0),(0,2,EStartPar 0),(1,3,EEndPar 0),(2,3,EEndPar 0)] 0 3 "x"
|
||||
|
||||
,test "Written to in all (two) IF guards, then self-assign" $ wrap $
|
||||
oSEQ [
|
||||
decl (return A.Int) oX [
|
||||
oIF [
|
||||
ifChoice (False, oX *:= return (3::Int))
|
||||
,ifChoice (False, oX *:= return (4::Int))
|
||||
]
|
||||
]
|
||||
,oX *:= oX
|
||||
]
|
||||
,testWarn "Written to in only one IF guards, then self-assign" $ wrap $
|
||||
oSEQ [
|
||||
decl (return A.Int) oX [
|
||||
oIF [
|
||||
ifChoice (False, oX *:= return (3::Int))
|
||||
,ifChoice (False, oSKIP)
|
||||
]
|
||||
]
|
||||
,oX *:= oX
|
||||
]
|
||||
,testWarn "Read from in last IF guards, then self-assign" $ wrap $
|
||||
oSEQ [
|
||||
decl (return A.Int) oX [
|
||||
oIF [
|
||||
ifChoice (False, oX *:= return (3::Int))
|
||||
,ifChoice (oX, oX *:= return (4::Int))
|
||||
]
|
||||
]
|
||||
,oX *:= oX
|
||||
]
|
||||
|
||||
-- Test loops (0 -> 1, 1 -> 2 -> 3 -> 1, 1 -> 4)
|
||||
-- Loop, nothing happens:
|
||||
|
|
|
|||
|
|
@ -17,13 +17,15 @@ with this program. If not, see <http://www.gnu.org/licenses/>.
|
|||
-}
|
||||
|
||||
-- | The necessary components for using an occam EDSL (for building test-cases).
|
||||
module OccamEDSL (ExpInp, ExpInpT, oSEQ, oPAR, oPROC, oSKIP, oINT,
|
||||
oCASE, oCASEinput, oALT, guard,
|
||||
module OccamEDSL (ExpInp, ExpInpT,
|
||||
oSEQ, oPAR, oPROC, oSKIP, oINT,
|
||||
oCASE, oCASEinput, caseOption, inputCaseOption,
|
||||
oALT, guard,
|
||||
oIF, ifChoice,
|
||||
Occ, oA, oB, oC, oX, oY, oZ, p0, p1, p2, (*?), (*!), (*:=), (*+), decl, decl', decl'',
|
||||
oempty, testOccamPass,
|
||||
oprocess,
|
||||
testOccamPassWarn, testOccamPassTransform, ExpInpC(shouldComeFrom),
|
||||
caseOption, inputCaseOption,
|
||||
becomes) where
|
||||
|
||||
import Control.Monad.State hiding (guard)
|
||||
|
|
@ -168,6 +170,15 @@ instance Castable (A.Structured A.Variant) A.Variant where
|
|||
makeStruct = id
|
||||
makePlain = A.Only emptyMeta
|
||||
|
||||
instance Castable A.Choice A.Choice where
|
||||
makeStruct = A.Only emptyMeta
|
||||
makePlain = id
|
||||
|
||||
instance Castable (A.Structured A.Choice) A.Choice where
|
||||
makeStruct = id
|
||||
makePlain = A.Only emptyMeta
|
||||
|
||||
|
||||
p0, p1, p2 :: Castable c A.Process => O c
|
||||
p0 = return $ makePlain $ A.Skip emptyMeta
|
||||
p1 = return $ makePlain $ A.Seq emptyMeta (A.Several emptyMeta [])
|
||||
|
|
@ -209,6 +220,15 @@ guard (inp, body)
|
|||
body' <- body
|
||||
return $ A.Only emptyMeta $ A.Alternative m (A.True emptyMeta) v im body'
|
||||
|
||||
oIF :: Castable c A.Process => [O (A.Structured A.Choice)] -> O c
|
||||
oIF = liftM (makePlain . A.If emptyMeta . singlify . A.Several emptyMeta) . sequence
|
||||
|
||||
ifChoice :: (CanBeExpression e, Castable c A.Choice) => (e, O A.Process) -> O c
|
||||
ifChoice (e, body)
|
||||
= do e' <- liftExpInp $ expr e
|
||||
body' <- body
|
||||
return $ makePlain $ A.Choice emptyMeta e' body'
|
||||
|
||||
singlify :: Data a => A.Structured a -> A.Structured a
|
||||
singlify (A.Several _ [s]) = s
|
||||
singlify ss = ss
|
||||
|
|
@ -246,17 +266,15 @@ oZ = return $ variable "Z"
|
|||
dest <- liftExpInp bdest >>* inputItem
|
||||
return $ makePlain $ A.Input emptyMeta ch dest
|
||||
|
||||
(*!), (*:=) :: CanBeExpression e => ExpInp A.Variable -> ExpInp e -> O (A.Structured A.Process)
|
||||
(*!), (*:=) :: (Castable r A.Process, CanBeExpression e) => ExpInp A.Variable -> ExpInp e -> O r
|
||||
(*!) bch bsrc = do
|
||||
ch <- liftExpInp bch
|
||||
src <- liftExpInp bsrc >>= (liftExpInp . expr)
|
||||
return $ A.Only emptyMeta $ A.Output emptyMeta ch [A.OutExpression emptyMeta
|
||||
src]
|
||||
return $ makePlain $ A.Output emptyMeta ch [A.OutExpression emptyMeta src]
|
||||
(*:=) bdest bsrc = do
|
||||
dest <- liftExpInp bdest
|
||||
src <- liftExpInp bsrc >>= (liftExpInp . expr)
|
||||
return $ A.Only emptyMeta $ A.Assign emptyMeta [dest] (A.ExpressionList emptyMeta
|
||||
[src])
|
||||
return $ makePlain $ A.Assign emptyMeta [dest] (A.ExpressionList emptyMeta [src])
|
||||
|
||||
infix 8 *:=
|
||||
|
||||
|
|
@ -307,6 +325,10 @@ instance CanBeExpression A.Expression where
|
|||
instance CanBeExpression Int where
|
||||
expr = return . A.Literal emptyMeta A.Int . A.IntLiteral emptyMeta . show
|
||||
|
||||
instance CanBeExpression Bool where
|
||||
expr True = return $ A.True emptyMeta
|
||||
expr False = return $ A.False emptyMeta
|
||||
|
||||
instance CanBeExpression e => CanBeExpression (ExpInp e) where
|
||||
expr = join . liftM expr
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user