Skip to content

Commit c2762e3

Browse files
RussoulRussoul
committed
Tests
1 parent 83a6450 commit c2762e3

20 files changed

Lines changed: 199 additions & 92 deletions

File tree

‎bench/cardano-recon-framework/app/Cardano/ReCon/Common.hs‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,14 +9,14 @@ import Data.Map.Strict (Map)
99
import Data.Text (Text)
1010

1111
-- | Extract integer properties from a JSON object.
12-
extractIntProps :: Object -> Map PropVarIdentifier IntValue
12+
extractIntProps :: Object -> Map VariableIdentifier IntValue
1313
extractIntProps = Map.delete "kind" . Map.mapMaybe f . Map.mapKeysMonotonic toText . KeyMap.toMap
1414
where
1515
f (Number v) = Just (truncate v)
1616
f _ = Nothing
1717

1818
-- | Extract text properties from a JSON object.
19-
extractTextProps :: Object -> Map PropVarIdentifier Text
19+
extractTextProps :: Object -> Map VariableIdentifier Text
2020
extractTextProps = Map.delete "kind" . Map.mapMaybe f . Map.mapKeysMonotonic toText . KeyMap.toMap
2121
where
2222
f (String v) = Just v

‎bench/cardano-recon-framework/examples/run.txt‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
Example trace tests for cardano-recon
2+
======================================
3+
4+
Working directory: bench/cardano-recon-framework
5+
Build: nix develop -c bash -c "cd bench/cardano-recon-framework && cabal build cardano-recon"
6+
7+
Each test runs:
8+
cabal run cardano-recon -- examples/cfgs/formulas.yaml
9+
--mode offline --duration 10 --timeunit second
10+
<trace>
11+
12+
Positive traces — every formula must produce (✔), none must produce (✗):
13+
examples/extracts/ok-1.txt
14+
examples/extracts/ok-2.txt
15+
examples/extracts/ok-3.txt
16+
examples/extracts/ok-4.txt
17+
18+
Negative traces — at least one formula must produce (✗):
19+
examples/extracts/fail-1.txt
20+
examples/extracts/fail-2.txt
21+
examples/extracts/fail-3.txt

‎bench/cardano-recon-framework/src/Cardano/ReCon/Common/Types.hs‎

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,12 @@
1-
module Cardano.ReCon.Common.Types (IntValue) where
1+
module Cardano.ReCon.Common.Types (IntValue, VariableIdentifier) where
22

33
import Data.Int (Int64)
4+
import Data.Text (Text)
45

56
-- | The numeric type used for integer event property values and polynomial
67
-- arithmetic throughout the framework.
78
type IntValue = Int64
9+
10+
-- | The type of variable identifiers used throughout the framework
11+
-- (LTL property variables and polynomial integer variables).
12+
type VariableIdentifier = Text

‎bench/cardano-recon-framework/src/Cardano/ReCon/Integer/Polynomial/Parser.hs‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
module Cardano.ReCon.Integer.Polynomial.Parser (Parser, identifier, integer, nat, intTerm) where
22

3-
import Cardano.ReCon.Integer.Polynomial.Term (IntIdentifier, IntTerm (..), mulTerm)
3+
import Cardano.ReCon.Integer.Polynomial.Term (VariableIdentifier, IntTerm (..), mulTerm)
44

55
import Data.Char (isAlpha, isAlphaNum)
66
import Data.Int (Int64)
@@ -16,7 +16,7 @@ type Parser = Parsec Void Text
1616

1717
-- | An identifier: starts with letter or underscore, continues with
1818
-- alphanumerics and underscores.
19-
identifier :: Parser IntIdentifier
19+
identifier :: Parser VariableIdentifier
2020
identifier =
2121
Text.pack <$> ((:) <$> firstChar <*> many nextChar) <?> "identifier"
2222
where

‎bench/cardano-recon-framework/src/Cardano/ReCon/Integer/Polynomial/Term.hs‎

Lines changed: 3 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,14 @@
11
module Cardano.ReCon.Integer.Polynomial.Term (
2-
IntIdentifier
2+
VariableIdentifier
33
, IntValue
44
, IntTerm(..)
55
, mulTerm
66
) where
77

8-
import Cardano.ReCon.Common.Types (IntValue)
9-
10-
import Data.Text (Text)
11-
12-
type IntIdentifier = Text
8+
import Cardano.ReCon.Common.Types (IntValue, VariableIdentifier)
139

1410
-- | i, j ::= i + i | <int> · x | <int>, where <int> is an arbitrary integer
15-
data IntTerm = IntVar IntValue IntIdentifier | IntConst IntValue | IntSum IntTerm IntTerm deriving (Show, Eq, Ord)
11+
data IntTerm = IntVar IntValue VariableIdentifier | IntConst IntValue | IntSum IntTerm IntTerm deriving (Show, Eq, Ord)
1612

1713
-- k · i
1814
-- k · (k' · x) = (k * k') · x

‎bench/cardano-recon-framework/src/Cardano/ReCon/Integer/Polynomial/Value.hs‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ module Cardano.ReCon.Integer.Polynomial.Value (
1212
, normalise
1313
) where
1414

15-
import Cardano.ReCon.Integer.Polynomial.Term (IntIdentifier, IntTerm (..), IntValue)
15+
import Cardano.ReCon.Integer.Polynomial.Term (VariableIdentifier, IntTerm (..), IntValue)
1616

1717
import qualified Data.List as List
1818
import Data.Map.Strict (Map)
@@ -21,7 +21,7 @@ import qualified Data.Map.Strict as Map
2121
-- | c + k₀ · x₀ + k₁ · x₁ + ... + kₙ · xₙ
2222
data IntTermNF = IntTermNF {
2323
-- | Invariant: the coefficients must be non-zero.
24-
coeff :: Map IntIdentifier IntValue,
24+
coeff :: Map VariableIdentifier IntValue,
2525
constant :: IntValue
2626
} deriving (Show, Eq, Ord)
2727

@@ -46,10 +46,10 @@ minus IntTermNF{coeff, constant} IntTermNF{coeff = coeff', constant = constant'}
4646
mul :: IntValue -> IntTermNF -> IntTermNF
4747
mul k IntTermNF{..} = IntTermNF{constant = k * constant, coeff = Map.filter (/= 0) $ Map.map (* k) coeff}
4848

49-
setCoeff :: IntValue -> IntIdentifier -> IntTermNF -> IntTermNF
49+
setCoeff :: IntValue -> VariableIdentifier -> IntTermNF -> IntTermNF
5050
setCoeff k x IntTermNF{..} = IntTermNF{coeff = Map.filter (/= 0) $ Map.insert x k coeff, constant}
5151

52-
nullify :: IntIdentifier -> IntTermNF -> IntTermNF
52+
nullify :: VariableIdentifier -> IntTermNF -> IntTermNF
5353
nullify = setCoeff 0
5454

5555
-- TODO: Rename to eval to conform with other similar functions

‎bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Check.hs‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -19,35 +19,35 @@ import Data.Text (Text)
1919

2020
-- The file concerns checking syntactic correctness of formulas.
2121

22-
data Error = UnboundPropVarIdentifier PropVarIdentifier deriving (Show, Eq)
22+
data Error = UnboundVariableIdentifier VariableIdentifier deriving (Show, Eq)
2323

2424
prettyError :: Error -> Text
25-
prettyError (UnboundPropVarIdentifier x) = "Unbound property variable: " <> x
25+
prettyError (UnboundVariableIdentifier x) = "Unbound property variable: " <> x
2626

2727
-- | Verify the given parameter variable is bound in the current context.
28-
checkParamVar :: Set PropVarIdentifier -> Text -> [Error]
28+
checkParamVar :: Set VariableIdentifier -> Text -> [Error]
2929
checkParamVar bound x | member x bound = []
30-
checkParamVar _ x = [UnboundPropVarIdentifier x]
30+
checkParamVar _ x = [UnboundVariableIdentifier x]
3131

3232
-- | Validate an integer term by checking all of its free variables are bound.
33-
checkIntTerm :: Set PropVarIdentifier -> IntTerm -> [Error]
33+
checkIntTerm :: Set VariableIdentifier -> IntTerm -> [Error]
3434
checkIntTerm bound (IntVar _ x) = checkParamVar bound x
3535
checkIntTerm _ (IntConst _) = []
3636
checkIntTerm bound (IntSum a b) = checkIntTerm bound a ++ checkIntTerm bound b
3737

3838
-- | Validate a text term by checking all of its free variables are bound.
39-
checkTextTerm :: Set PropVarIdentifier -> TextTerm -> [Error]
39+
checkTextTerm :: Set VariableIdentifier -> TextTerm -> [Error]
4040
checkTextTerm bound (TextVar x) = checkParamVar bound x
4141
checkTextTerm _ (TextConst _) = []
4242

4343
-- | Validate a constraint by ensuring its term is well-scoped.
44-
checkParamConstraint :: Set PropVarIdentifier -> PropConstraint -> [Error]
44+
checkParamConstraint :: Set VariableIdentifier -> PropConstraint -> [Error]
4545
checkParamConstraint bound (IntPropConstraint _ t) = checkIntTerm bound t
4646
checkParamConstraint bound (TextPropConstraint _ t) = checkTextTerm bound t
4747

4848
-- | Check whether the formula is syntactically valid:
4949
-- | — all parameter variables shall be universally bound
50-
checkFormula :: Set PropVarIdentifier -> Formula event ty -> [Error]
50+
checkFormula :: Set VariableIdentifier -> Formula event ty -> [Error]
5151
checkFormula bound (Forall _ phi) = checkFormula bound phi
5252
checkFormula bound (ForallN _ phi) = checkFormula bound phi
5353
checkFormula bound (ExistsN _ phi) = checkFormula bound phi

‎bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Lang/Formula.hs‎

Lines changed: 14 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
module Cardano.ReCon.LTL.Lang.Formula (
22
PropName
3-
, PropVarIdentifier
3+
, VariableIdentifier
44
, IntValue
55
, TextValue
66
, IntTerm(..)
@@ -22,7 +22,7 @@ module Cardano.ReCon.LTL.Lang.Formula (
2222
import Prelude hiding (and)
2323

2424
import Cardano.ReCon.Common.BinRel (BinRel (..))
25-
import Cardano.ReCon.Common.Types (IntValue)
25+
import Cardano.ReCon.Common.Types (IntValue, VariableIdentifier)
2626
import Cardano.ReCon.Integer.Polynomial.Term (IntTerm (..))
2727

2828
import Data.Map.Strict (Map)
@@ -33,15 +33,11 @@ import Data.Word (Word64)
3333
-- | A property name (e.g. "thread", "node", etc.).
3434
type PropName = Text
3535

36-
-- | Default name: x.
37-
-- | Identifier denoting an event property variable.
38-
type PropVarIdentifier = Text
39-
4036
-- | Text event property value.
4137
type TextValue = Text
4238

4339
-- | Text term: a constant string or a variable ranging over strings.
44-
data TextTerm = TextConst Text | TextVar PropVarIdentifier deriving (Show, Eq, Ord)
40+
data TextTerm = TextConst TextValue | TextVar VariableIdentifier deriving (Show, Eq, Ord)
4541

4642
-- | Default name: c.
4743
-- | A constraint inside an `Atom`, matching an event property against a term.
@@ -110,25 +106,25 @@ data Formula event ty =
110106

111107
----------- Event property ----------
112108
-- | ∀x : Int. φ — x ranges over all integers
113-
| PropIntForall PropVarIdentifier (Formula event ty)
109+
| PropIntForall VariableIdentifier (Formula event ty)
114110
-- | ∀x : Text. φ — x ranges over all strings
115-
| PropTextForall PropVarIdentifier (Formula event ty)
111+
| PropTextForall VariableIdentifier (Formula event ty)
116112
-- | ∀x ∈ v̄. φ — x ranges over the given integers
117-
| PropIntForallN PropVarIdentifier (Set IntValue) (Formula event ty)
113+
| PropIntForallN VariableIdentifier (Set IntValue) (Formula event ty)
118114
-- | ∀x ∈ v̄. φ — x ranges over the given strings
119-
| PropTextForallN PropVarIdentifier (Set Text) (Formula event ty)
115+
| PropTextForallN VariableIdentifier (Set TextValue) (Formula event ty)
120116
-- | ∃x : Int. φ — x ranges over all integers
121-
| PropIntExists PropVarIdentifier (Formula event ty)
117+
| PropIntExists VariableIdentifier (Formula event ty)
122118
-- | ∃x : Text. φ — x ranges over all strings
123-
| PropTextExists PropVarIdentifier (Formula event ty)
119+
| PropTextExists VariableIdentifier (Formula event ty)
124120
-- | ∃x ∈ v̄. φ — x ranges over the given integers
125-
| PropIntExistsN PropVarIdentifier (Set IntValue) (Formula event ty)
121+
| PropIntExistsN VariableIdentifier (Set IntValue) (Formula event ty)
126122
-- | ∃x ∈ v̄. φ — x ranges over the given strings
127-
| PropTextExistsN PropVarIdentifier (Set Text) (Formula event ty)
123+
| PropTextExistsN VariableIdentifier (Set TextValue) (Formula event ty)
128124
-- | t rel t (integer)
129125
| PropIntBinRel BinRel (Relevance event ty) IntTerm IntTerm
130126
-- | t = v (text)
131-
| PropTextEq (Relevance event ty) TextTerm Text
127+
| PropTextEq (Relevance event ty) TextTerm TextValue
132128
-------------------------------------
133129
deriving (Show, Eq, Ord)
134130

@@ -230,9 +226,9 @@ class Event a ty | a -> ty where
230226
ofTy :: a -> ty -> Bool
231227
-- | Integer properties of the event pertinent to the given type.
232228
-- intProps e t assumes that ofTy e t = True
233-
intProps :: a -> ty -> Map PropVarIdentifier IntValue
229+
intProps :: a -> ty -> Map VariableIdentifier IntValue
234230
-- | Text properties of the event pertinent to the given type.
235231
-- textProps e t assumes that ofTy e t = True
236-
textProps :: a -> ty -> Map PropVarIdentifier Text
232+
textProps :: a -> ty -> Map VariableIdentifier TextValue
237233
-- | Timestamp of the event in μs (Used for debug & monitoring only).
238234
beg :: a -> Word64

‎bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Lang/Formula/Parser.hs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,7 @@ data Domain = IntDomain (Set IntValue) | TextDomain (Set Text) deriving (Show, E
3636
data Context = Context {
3737
interpDomain :: [(Text, Domain)],
3838
-- | Kinds of in-scope property variables, populated by quantifier parsers.
39-
varKinds :: Map PropVarIdentifier PropKind
39+
varKinds :: Map VariableIdentifier PropKind
4040
}
4141

4242
unescapedVariableIdentifierNextChar :: Parser Char

‎bench/cardano-recon-framework/src/Cardano/ReCon/LTL/Lang/HomogeneousFormula.hs‎

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ module Cardano.ReCon.LTL.Lang.HomogeneousFormula (
1010
, normaliseHomogeneous) where
1111

1212
import Cardano.ReCon.Common.BinRel (BinRel (..))
13-
import Cardano.ReCon.LTL.Lang.Formula (Formula, IntTerm (..), IntValue, TextTerm (..), PropVarIdentifier)
13+
import Cardano.ReCon.LTL.Lang.Formula (Formula, IntTerm (..), IntValue, TextTerm (..), VariableIdentifier)
1414
import qualified Cardano.ReCon.LTL.Lang.Formula as F
1515
import Cardano.ReCon.LTL.Lang.HomogeneousFormula.IR.FinFree (Extended (..))
1616
import qualified Cardano.ReCon.LTL.Lang.HomogeneousFormula.IR.FinFree as FinFree
@@ -34,14 +34,14 @@ data HomogeneousFormula =
3434
-------------------------------------
3535

3636
----------- Event property ----------
37-
| PropIntForall PropVarIdentifier HomogeneousFormula
38-
| PropTextForall PropVarIdentifier HomogeneousFormula
39-
| PropIntForallN PropVarIdentifier (Set IntValue) HomogeneousFormula
40-
| PropTextForallN PropVarIdentifier (Set Text) HomogeneousFormula
41-
| PropIntExists PropVarIdentifier HomogeneousFormula
42-
| PropTextExists PropVarIdentifier HomogeneousFormula
43-
| PropIntExistsN PropVarIdentifier (Set IntValue) HomogeneousFormula
44-
| PropTextExistsN PropVarIdentifier (Set Text) HomogeneousFormula
37+
| PropIntForall VariableIdentifier HomogeneousFormula
38+
| PropTextForall VariableIdentifier HomogeneousFormula
39+
| PropIntForallN VariableIdentifier (Set IntValue) HomogeneousFormula
40+
| PropTextForallN VariableIdentifier (Set Text) HomogeneousFormula
41+
| PropIntExists VariableIdentifier HomogeneousFormula
42+
| PropTextExists VariableIdentifier HomogeneousFormula
43+
| PropIntExistsN VariableIdentifier (Set IntValue) HomogeneousFormula
44+
| PropTextExistsN VariableIdentifier (Set Text) HomogeneousFormula
4545
| PropIntBinRel BinRel IntTerm IntTerm
4646
| PropTextEq TextTerm Text
4747
deriving (Show, Eq, Ord)
@@ -109,7 +109,7 @@ equiv = on (==) eval
109109

110110
retract :: Formula event ty -> Maybe HomogeneousFormula
111111
retract = go Set.empty where
112-
go :: Set PropVarIdentifier -> Formula event ty -> Maybe HomogeneousFormula
112+
go :: Set VariableIdentifier -> Formula event ty -> Maybe HomogeneousFormula
113113
go _ (F.ForallN {}) = Nothing
114114
go _ (F.ExistsN {}) = Nothing
115115
go _ (F.Forall {}) = Nothing
@@ -138,7 +138,7 @@ retract = go Set.empty where
138138
go bound (F.PropTextExists x phi) = PropTextExists x <$> go (Set.insert x bound) phi
139139
go bound (F.PropIntExistsN x dom phi) = PropIntExistsN x dom <$> go (Set.insert x bound) phi
140140
go bound (F.PropTextExistsN x dom phi) = PropTextExistsN x dom <$> go (Set.insert x bound) phi
141-
groundTerm :: Set PropVarIdentifier -> IntTerm -> Bool
141+
groundTerm :: Set VariableIdentifier -> IntTerm -> Bool
142142
groundTerm _ (IntConst _) = True
143143
groundTerm bound' (IntVar _ x) = Set.member x bound'
144144
groundTerm bound' (IntSum a b) = groundTerm bound' a && groundTerm bound' b

0 commit comments

Comments
 (0)