spectacle-1.0.0: spectacle.cabal
cabal-version: 2.4
name: spectacle
version: 1.0.0
category: Testing, Concurrency
synopsis: Embedded specification language & model checker in Haskell.
description:
Spectacle is an embedded domain-specific language that provides a family
of type-level combinators for authoring specifications of program behavior
along with a model checker for verifying that user implementations of a
program satisfy written specifications.
author: Arista Networks
maintainer: opensource@awakesecurity.com
homepage: https://github.com/awakesecurity/spectacle
bug-reports: https://github.com/awakesecurity/spectacle/issues
license: Apache-2.0
license-file: LICENSE
copyright: 2021 Arista Networks
build-type: Simple
tested-with:
GHC == 8.10.3
extra-source-files:
README.md
CHANGELOG.md
common common
default-language: Haskell2010
ghc-options:
-Wall
-Wcompat
-Wincomplete-record-updates
-Wincomplete-uni-patterns
-Wmissing-fields
-Wpartial-fields
-Widentities
-Wmissing-home-modules
-Wredundant-constraints
-fshow-warning-groups
-Wmissing-import-lists
-Wunused-packages
build-depends:
base >=4.14 && <4.15
default-extensions:
BangPatterns BlockArguments ConstraintKinds DataKinds DefaultSignatures
DeriveFunctor DeriveGeneric DerivingVia FlexibleContexts FlexibleInstances
GADTs LambdaCase MagicHash MultiParamTypeClasses PatternSynonyms PolyKinds
RankNTypes RoleAnnotations ScopedTypeVariables StandaloneDeriving
StandaloneKindSignatures TypeApplications TypeOperators UnicodeSyntax
ViewPatterns
library
import: common
hs-source-dirs: src
build-depends:
comonad
, containers >= 0.6
, hashable >= 1.3.0.0
, microlens
, microlens-mtl
, mtl >= 2.2
, optparse-applicative
, logict
, prettyprinter
, prettyprinter-ansi-terminal
, text
, transformers >= 0.5
exposed-modules:
Control.Applicative.Day
, Control.Applicative.Phases
, Control.Applicative.Queue
, Control.Comonad.Tape
, Control.Hyper
, Control.Mealy
, Control.Monad.Levels
, Control.Monad.Levels.Internal
, Control.Monad.Ref
, Control.Natural
, Data.Ascript
, Data.Bag
, Data.Fingerprint
, Data.Functor.Loom
, Data.Functor.Tree
, Data.Name
, Data.Node
, Data.Type.List
, Data.Type.Rec
, Data.World
, Language.Spectacle
, Language.Spectacle.AST
, Language.Spectacle.AST.Action
, Language.Spectacle.AST.Temporal
, Language.Spectacle.Exception.RuntimeException
, Language.Spectacle.Fairness
, Language.Spectacle.Interaction
, Language.Spectacle.Interaction.CLI
, Language.Spectacle.Interaction.Diagram
, Language.Spectacle.Interaction.Doc
, Language.Spectacle.Interaction.Options
, Language.Spectacle.Interaction.Paths
, Language.Spectacle.Interaction.Point
, Language.Spectacle.Interaction.Pos
, Language.Spectacle.Model
, Language.Spectacle.Model.ModelAction
, Language.Spectacle.Model.ModelEnv
, Language.Spectacle.Model.ModelError
, Language.Spectacle.Model.ModelNode
, Language.Spectacle.Model.ModelState
, Language.Spectacle.Model.ModelTemporal
, Language.Spectacle.Model.Monad
, Language.Spectacle.Lang
, Language.Spectacle.Lang.Internal
, Language.Spectacle.Lang.Member
, Language.Spectacle.Lang.Op
, Language.Spectacle.Lang.Scoped
, Language.Spectacle.RTS.Registers
, Language.Spectacle.Specification
, Language.Spectacle.Specification.Action
, Language.Spectacle.Specification.Prop
, Language.Spectacle.Specification.Variable
, Language.Spectacle.Syntax
, Language.Spectacle.Syntax.Closure
, Language.Spectacle.Syntax.Closure.Internal
, Language.Spectacle.Syntax.Enabled
, Language.Spectacle.Syntax.Enabled.Internal
, Language.Spectacle.Syntax.Env
, Language.Spectacle.Syntax.Env.Internal
, Language.Spectacle.Syntax.Error
, Language.Spectacle.Syntax.Error.Internal
, Language.Spectacle.Syntax.NonDet
, Language.Spectacle.Syntax.NonDet.Internal
, Language.Spectacle.Syntax.Plain
, Language.Spectacle.Syntax.Plain.Internal
, Language.Spectacle.Syntax.Prime
, Language.Spectacle.Syntax.Prime.Internal
, Language.Spectacle.Syntax.Quantifier
, Language.Spectacle.Syntax.Quantifier.Internal
, Language.Spectacle.Syntax.Logic
, Language.Spectacle.Syntax.Logic.Internal
test-suite unit-tests
import: common
type: exitcode-stdio-1.0
hs-source-dirs: test/unit-tests
main-is: Main.hs
other-modules:
Test.Control.Comonad.Tape
Test.Gen
Test.Gen.Rec
Test.Language.Spectacle.Interaction
Test.Language.Spectacle.Interaction.Paths
Test.Language.Spectacle.Interaction.Pos
Test.Laws.Lens
Test.Laws.Ord
build-depends:
comonad
, containers
, spectacle
, hedgehog
, microlens
, tasty
, tasty-hedgehog
test-suite integration-tests
import: common
type: exitcode-stdio-1.0
hs-source-dirs: test/integration
main-is: Main.hs
other-modules:
Specifications.BitClock
Specifications.Diehard
Specifications.SimpleClock
Specifications.Status
build-depends:
spectacle
, hashable
, hedgehog
, tasty
, tasty-hedgehog