awakesecurity / spectacle Goto Github PK

Embedded specification language & model checker in Haskell

License: Apache License 2.0

Haskell 98.68% Nix 1.13% Shell 0.19%

spectacle's Introduction

spectacle

Language.Spectacle defines an embedded language for writing formal specifications of software in the temporal logic of actions. Specifications written in spectacle can be model-checked and shown to either be correct with respect to temporal properties or refuted by a counterexample. Examples of specifications written in spectacle are provided under test/integration.

spectacle's People

Contributors

Stargazers

Watchers

Forkers

ixmatus agentultra unshorn lemastero dannypsnl-fork bgohla mariszo 5l1v3r1 gusbicalho thoughtpolice nicolast proofconstruction

spectacle's Issues

The integration tests are not verified correctly

When run nix-build --attr spectacle in GitHub Action, the integration-tests suite looks passed but actually we have no guarantee. For example, I tried to simplify SimpleClock and tweak it into the trivially invalid spec, then the test passed.

type ClockSpec = '["hours" # Int]

initial :: Initial ClockSpec ()
initial = do
  #hours `define` return 0

action :: Action ClockSpec Bool
action = tick

tick :: Action ClockSpec Bool
tick = do
  hours <- plain #hours
  #hours .= return (hours + 1)
  return True

formula :: Invariant ClockSpec Bool
formula = always inBounds
  where
    inBounds :: Invariant ClockSpec Bool
    inBounds = do
      hours <- plain #hours
      -- Here is the stupid condition
      return False

check :: IO ()
check = do
  let spec :: Specification ClockSpec
      spec =
        Specification
          { initialAction = initial
          , nextAction = action
          , temporalFormula = formula
          , terminationFormula = Nothing
          , fairnessConstraint = weakFair
          }
  defaultInteraction (modelCheck spec)

Use `Managed` monad in CLI

Currently Language.Spectacle.Interaction.Options uses a file Handle to write model checker logs to a file if the user provides an output path with --output/-o and is subsequently closed when CLI is completed in Language.Spectacle.Interaction.CLI.

Manually managing this handle is error-prone. @ixmatus noted using the Managed monad to handle cleanup of file Handles would be an improvement.

Adding Spectacle to Hackage & nixpkgs?

Hi all, cool project, any plans to add it to Hackage and Nixpkgs? I see you're already Nix users.

I submitted a packaging request for it, and they asked me to check if it's being included Hackage, which would make it easier to add to nixpkgs.

Should --only-trace should imply --log when using `interaction`?

Consider the DieHard example. If you run it normally, the counterexample is generated. Running it with --only-trace, it obviously succeeds, but simply exits with

specification: trace: success

Now, if you look at the options, this is obvious, since it says it only traces behaviors and turns off model checking. But when I was first using Spectacle, I actually typo'd -t and -l several times which confused me: why did this succeed? Ignoring that entirely though, -t is practically useless without -l because you literally can't see the traces without it. So I just always run with -tl most of the time until I want to check and just run it without either option (or I'm debugging.)

This is more of a UX question than anything: if we're just tracing without checks, should we always diagram the output traces? This will probably impact the Interaction API, of course...

Liveness property checked incorrectly

Hello! First of all, impressive work with his library. Thanks for releasing it.

I was trying to port some stuff from TLA+ to Spectacle and run into some weird behaviour with eventually and eventually . always properties.

The test file below reproduces the issues.

The expected behaviour of the model is that a Right counter value will be incremented until it gets to the maxCounter constant, and then it shifts to the final state Left counter. Thus, it should hold that #counter is eventually equal to Left maxCounter, and it is also the case that it eventually is always equal to Left counter. However, this property should be violated if the initialCounter value is larger than maxCounter.

What I see, though, is that eventually seems to reject cases where the model gets stuck forever in a state, even though that state matches the formula. On the other hand, it looks like eventually . always accepts possibilities that actually never achieve the desired state.

Of course it may be that I'm making a mistake using the library. If that's the case I would be very thankful if you could point me in the right direction.

Versions:

MacOS Mojave
GHC 8.10.7
Spectacle - git commit 7e7efd6

Test module

{-# LANGUAGE DataKinds, ImportQualifiedPost, OverloadedLabels, TypeOperators #-}

module Specs.SimpleCounterSpec where

import Data.Either qualified as Either
import Language.Spectacle (Action, Initial, Invariant, always, define, eventually, modelCheck, plain, weakFair, (.=), type (#))
import Language.Spectacle.Specification (Specification (..))
import Test.Hspec (Spec, describe, hspec, it, shouldSatisfy)

main :: IO ()
main = hspec spec

spec :: Spec
spec =
  describe "Counter spec" $ do
    describe "eventually is maxCounter" $ do
      let specification constants =
            Specification
              { initialAction = initSpec constants
              , nextAction = next
              , temporalFormula = eventually $ formula constants
              , terminationFormula = Nothing
              , fairnessConstraint = weakFair
              }
      it "passes when initialCounter < maxCounter" $ do
        modelCheck (specification (1, 4)) `shouldSatisfy` Either.isRight
      it "passes when initialCounter = maxCounter" $ do
        modelCheck (specification (4, 4)) `shouldSatisfy` Either.isRight
      it "fails when initialCounter > maxCounter" $ do
        modelCheck (specification (4, 2)) `shouldSatisfy` Either.isLeft
    describe "eventually always is maxCounter" $ do
      let specification constants =
            Specification
              { initialAction = initSpec constants
              , nextAction = next
              , temporalFormula = eventually . always $ formula constants
              , terminationFormula = Nothing
              , fairnessConstraint = weakFair
              }
      it "passes when initialCounter < maxCounter" $ do
        modelCheck (specification (1, 4)) `shouldSatisfy` Either.isRight
      it "passes when initialCounter = maxCounter" $ do
        modelCheck (specification (4, 4)) `shouldSatisfy` Either.isRight
      it "fails when initialCounter > maxCounter" $ do
        modelCheck (specification (4, 2)) `shouldSatisfy` Either.isLeft

type CounterSpec = '["goal" # Word, "counter" # Either Word Word]

initSpec :: (Word, Word) -> Initial CounterSpec ()
initSpec (initialCounter, maxCounter) = do
  #goal `define` pure maxCounter
  #counter `define` pure (Right initialCounter)

next :: Action CounterSpec Bool
next = do
  goal <- plain #goal
  counter <- plain #counter
  case counter of
    Right c
      | c < goal -> do
        #counter .= pure (Right $ c + 1)
        pure True
      | otherwise -> do
        #counter .= pure (Left c)
        pure True
    Left _ -> pure True

formula :: (Word, Word) -> Invariant CounterSpec Bool
formula (_, maxCounter) = do
  counter <- plain #counter
  pure $ counter == Left maxCounter

Output of test run:

Counter spec
  eventually is maxCounter
    passes when initialCounter < maxCounter [✘]
    passes when initialCounter = maxCounter [✘]
    fails when initialCounter > maxCounter [✔]
  eventually always is maxCounter
    passes when initialCounter < maxCounter [✔]
    passes when initialCounter = maxCounter [✔]
    fails when initialCounter > maxCounter [✘]

Failures:

  test/Specs/SimpleCounterSpec.hs:24:9: 
  1) Counter spec, eventually is maxCounter, passes when initialCounter < maxCounter
       predicate failed on: Left [MCFormulaError <<0x86c03a317:goal=4 counter=Left 4 RNil>> --> <<0x86c03a317:goal=4 counter=Left 4 RNil>> (Just (SrcLoc {srcLocPackage = "main", srcLocModule = "Specs.SimpleCounterSpec", srcLocFile = "test/Specs/SimpleCounterSpec.hs", srcLocStartLine = 19, srcLocStartCol = 35, srcLocEndLine = 19, srcLocEndCol = 65})) EventuallyPropK]

  To rerun use: --match "/Counter spec/eventually is maxCounter/passes when initialCounter < maxCounter/"

  test/Specs/SimpleCounterSpec.hs:26:9: 
  2) Counter spec, eventually is maxCounter, passes when initialCounter = maxCounter
       predicate failed on: Left [MCFormulaError <<0x86c03a317:goal=4 counter=Left 4 RNil>> --> <<0x86c03a317:goal=4 counter=Left 4 RNil>> (Just (SrcLoc {srcLocPackage = "main", srcLocModule = "Specs.SimpleCounterSpec", srcLocFile = "test/Specs/SimpleCounterSpec.hs", srcLocStartLine = 19, srcLocStartCol = 35, srcLocEndLine = 19, srcLocEndCol = 65})) EventuallyPropK]

  To rerun use: --match "/Counter spec/eventually is maxCounter/passes when initialCounter = maxCounter/"

  test/Specs/SimpleCounterSpec.hs:43:9: 
  3) Counter spec, eventually always is maxCounter, fails when initialCounter > maxCounter
       predicate failed on: Right (ModelMetrics {_distinctStates = 2, _treeDepth = 2, _treeWidth = 0})

  To rerun use: --match "/Counter spec/eventually always is maxCounter/fails when initialCounter > maxCounter/"

Randomized with seed 1147279803

Finished in 0.0219 seconds
6 examples, 3 failures
*** Exception: ExitFailure 1

Support GHC 9.0 / base 4.15

For packaging in nixpkgs (see NixOS/nixpkgs#135145), it'd be great to support GHC 9.0 and base 4.15, since we use them by default now. We can ship the package for GHC 8.10.7 for now, but it'd be good to have it in the default package set.

[ 1 of 71] Compiling Control.Applicative.Day ( src/Control/Applicative/Day.hs, dist/build/Control/Applicative/Day.o, dist/build/Control/Applicative/Day.dyn_o )
[ 2 of 71] Compiling Control.Applicative.Phases ( src/Control/Applicative/Phases.hs, dist/build/Control/Applicative/Phases.o, dist/build/Control/Applicative/Phases.dyn_o )
[ 3 of 71] Compiling Control.Applicative.Queue ( src/Control/Applicative/Queue.hs, dist/build/Control/Applicative/Queue.o, dist/build/Control/Applicative/Queue.dyn_o )

src/Control/Applicative/Queue.hs:27:42: error:
    • Couldn't match type: forall x. Phases f x -> Phases f (a, x)
                     with: Phases a0 () -> Phases f (a, b0)
      Expected: Day (Phases f) a -> Phases a0 () -> Phases f (a, b0)
        Actual: Day (Phases f) a
                -> forall x. Phases f x -> Phases f (a, x)
    • In the first argument of ‘flip’, namely ‘getDay’
      In the second argument of ‘(.)’, namely ‘flip getDay (Here ())’
      In the second argument of ‘(.)’, namely
        ‘lowerPhases . flip getDay (Here ())’
    • Relevant bindings include
        runQueue :: Queue f a -> f a
          (bound at src/Control/Applicative/Queue.hs:27:1)
   |
27 | runQueue = fmap fst . lowerPhases . flip getDay (Here ())
   |                                          ^^^^^^

src/Control/Applicative/Queue.hs:36:51: error:
    • Couldn't match type: forall x1. Phases f x1 -> Phases f (a, x1)
                     with: Phases f x -> Phases f (a, x)
      Expected: Day (Phases f) a -> Phases f x -> Phases f (a, x)
        Actual: Day (Phases f) a
                -> forall x. Phases f x -> Phases f (a, x)
    • In the second argument of ‘(.)’, namely ‘getDay’
      In the first argument of ‘fmap’, namely ‘(($ x) . getDay)’
      In the first argument of ‘wrapPhases’, namely
        ‘(fmap (($ x) . getDay) f)’
    • Relevant bindings include
        x :: Phases f x (bound at src/Control/Applicative/Queue.hs:36:20)
        f :: f (Queue f a)
          (bound at src/Control/Applicative/Queue.hs:36:11)
        wrapQueue :: f (Queue f a) -> Queue f a
          (bound at src/Control/Applicative/Queue.hs:36:1)
   |
36 | wrapQueue f = Day \x -> wrapPhases (fmap (($ x) . getDay) f)
   |                                                   ^^^^^^
[ 4 of 71] Compiling Control.Comonad.Tape ( src/Control/Comonad/Tape.hs, dist/build/Control/Comonad/Tape.o, dist/build/Control/Comonad/Tape.dyn_o )
[ 5 of 71] Compiling Control.Hyper    ( src/Control/Hyper.hs, dist/build/Control/Hyper.o, dist/build/Control/Hyper.dyn_o )
[ 6 of 71] Compiling Control.Mealy    ( src/Control/Mealy.hs, dist/build/Control/Mealy.o, dist/build/Control/Mealy.dyn_o )
[ 7 of 71] Compiling Control.Monad.Ref ( src/Control/Monad/Ref.hs, dist/build/Control/Monad/Ref.o, dist/build/Control/Monad/Ref.dyn_o )
[ 8 of 71] Compiling Control.Natural  ( src/Control/Natural.hs, dist/build/Control/Natural.o, dist/build/Control/Natural.dyn_o )
[ 9 of 71] Compiling Data.Ascript     ( src/Data/Ascript.hs, dist/build/Data/Ascript.o, dist/build/Data/Ascript.dyn_o )
[10 of 71] Compiling Data.Functor.Loom ( src/Data/Functor/Loom.hs, dist/build/Data/Functor/Loom.o, dist/build/Data/Functor/Loom.dyn_o )
[12 of 71] Compiling Data.Name        ( src/Data/Name.hs, dist/build/Data/Name.o, dist/build/Data/Name.dyn_o )
[13 of 71] Compiling Data.Node        ( src/Data/Node.hs, dist/build/Data/Node.o, dist/build/Data/Node.dyn_o )
[14 of 71] Compiling Data.Bag         ( src/Data/Bag.hs, dist/build/Data/Bag.o, dist/build/Data/Bag.dyn_o )
[15 of 71] Compiling Control.Monad.Levels.Internal ( src/Control/Monad/Levels/Internal.hs, dist/build/Control/Monad/Levels/Internal.o, dist/build/Control/Monad/Levels/Internal.dyn_o )
[16 of 71] Compiling Control.Monad.Levels ( src/Control/Monad/Levels.hs, dist/build/Control/Monad/Levels.o, dist/build/Control/Monad/Levels.dyn_o )
[17 of 71] Compiling Data.Type.List   ( src/Data/Type/List.hs, dist/build/Data/Type/List.o, dist/build/Data/Type/List.dyn_o )
[18 of 71] Compiling Data.Type.Rec    ( src/Data/Type/Rec.hs, dist/build/Data/Type/Rec.o, dist/build/Data/Type/Rec.dyn_o )
[19 of 71] Compiling Data.Fingerprint ( src/Data/Fingerprint.hs, dist/build/Data/Fingerprint.o, dist/build/Data/Fingerprint.dyn_o )
[20 of 71] Compiling Data.World       ( src/Data/World.hs, dist/build/Data/World.o, dist/build/Data/World.dyn_o )
[21 of 71] Compiling Language.Spectacle.Exception.RuntimeException ( src/Language/Spectacle/Exception/RuntimeException.hs, dist/build/Language/Spectacle/Exception/RuntimeException.o, dist/build/Language/Spectacle/Exception/RuntimeException.dyn_o )
[22 of 71] Compiling Language.Spectacle.Fairness ( src/Language/Spectacle/Fairness.hs, dist/build/Language/Spectacle/Fairness.o, dist/build/Language/Spectacle/Fairness.dyn_o )

src/Language/Spectacle/Fairness.hs:40:40: error:
    • Syntax error on 'StrongFair
      Perhaps you intended to use TemplateHaskell or TemplateHaskellQuotes
    • In the Template Haskell quotation 'StrongFair
   |
40 |     strongTyCon = someTypeRep (Proxy @ 'StrongFair)
   |                                        ^^^^^^^^^^^
[23 of 71] Compiling Language.Spectacle.Interaction.Doc ( src/Language/Spectacle/Interaction/Doc.hs, dist/build/Language/Spectacle/Interaction/Doc.o, dist/build/Language/Spectacle/Interaction/Doc.dyn_o )
[24 of 71] Compiling Language.Spectacle.Interaction.Options ( src/Language/Spectacle/Interaction/Options.hs, dist/build/Language/Spectacle/Interaction/Options.o, dist/build/Language/Spectacle/Interaction/Options.dyn_o )
[25 of 71] Compiling Language.Spectacle.Interaction.CLI ( src/Language/Spectacle/Interaction/CLI.hs, dist/build/Language/Spectacle/Interaction/CLI.o, dist/build/Language/Spectacle/Interaction/CLI.dyn_o )
[26 of 71] Compiling Language.Spectacle.Interaction.Pos ( src/Language/Spectacle/Interaction/Pos.hs, dist/build/Language/Spectacle/Interaction/Pos.o, dist/build/Language/Spectacle/Interaction/Pos.dyn_o )
[27 of 71] Compiling Language.Spectacle.Interaction.Point ( src/Language/Spectacle/Interaction/Point.hs, dist/build/Language/Spectacle/Interaction/Point.o, dist/build/Language/Spectacle/Interaction/Point.dyn_o )
[30 of 71] Compiling Language.Spectacle.Lang.Op ( src/Language/Spectacle/Lang/Op.hs, dist/build/Language/Spectacle/Lang/Op.o, dist/build/Language/Spectacle/Lang/Op.dyn_o )
[31 of 71] Compiling Language.Spectacle.Lang.Scoped ( src/Language/Spectacle/Lang/Scoped.hs, dist/build/Language/Spectacle/Lang/Scoped.o, dist/build/Language/Spectacle/Lang/Scoped.dyn_o )
[32 of 71] Compiling Language.Spectacle.Lang.Member ( src/Language/Spectacle/Lang/Member.hs, dist/build/Language/Spectacle/Lang/Member.o, dist/build/Language/Spectacle/Lang/Member.dyn_o )
[33 of 71] Compiling Language.Spectacle.Model.ModelNode ( src/Language/Spectacle/Model/ModelNode.hs, dist/build/Language/Spectacle/Model/ModelNode.o, dist/build/Language/Spectacle/Model/ModelNode.dyn_o )
[34 of 71] Compiling Language.Spectacle.Model.ModelState ( src/Language/Spectacle/Model/ModelState.hs, dist/build/Language/Spectacle/Model/ModelState.o, dist/build/Language/Spectacle/Model/ModelState.dyn_o )
[35 of 71] Compiling Language.Spectacle.Syntax.NonDet.Internal ( src/Language/Spectacle/Syntax/NonDet/Internal.hs, dist/build/Language/Spectacle/Syntax/NonDet/Internal.o, dist/build/Language/Spectacle/Syntax/NonDet/Internal.dyn_o )
[36 of 71] Compiling Language.Spectacle.Lang.Internal ( src/Language/Spectacle/Lang/Internal.hs, dist/build/Language/Spectacle/Lang/Internal.o, dist/build/Language/Spectacle/Lang/Internal.dyn_o )
[37 of 71] Compiling Language.Spectacle.Lang ( src/Language/Spectacle/Lang.hs, dist/build/Language/Spectacle/Lang.o, dist/build/Language/Spectacle/Lang.dyn_o )
[38 of 71] Compiling Language.Spectacle.Syntax.NonDet ( src/Language/Spectacle/Syntax/NonDet.hs, dist/build/Language/Spectacle/Syntax/NonDet.o, dist/build/Language/Spectacle/Syntax/NonDet.dyn_o )
[39 of 71] Compiling Language.Spectacle.Syntax.Logic.Internal ( src/Language/Spectacle/Syntax/Logic/Internal.hs, dist/build/Language/Spectacle/Syntax/Logic/Internal.o, dist/build/Language/Spectacle/Syntax/Logic/Internal.dyn_o )
[40 of 71] Compiling Language.Spectacle.Syntax.Error.Internal ( src/Language/Spectacle/Syntax/Error/Internal.hs, dist/build/Language/Spectacle/Syntax/Error/Internal.o, dist/build/Language/Spectacle/Syntax/Error/Internal.dyn_o )
[41 of 71] Compiling Language.Spectacle.Syntax.Error ( src/Language/Spectacle/Syntax/Error.hs, dist/build/Language/Spectacle/Syntax/Error.o, dist/build/Language/Spectacle/Syntax/Error.dyn_o )
[42 of 71] Compiling Language.Spectacle.Syntax.Logic ( src/Language/Spectacle/Syntax/Logic.hs, dist/build/Language/Spectacle/Syntax/Logic.o, dist/build/Language/Spectacle/Syntax/Logic.dyn_o )
[43 of 71] Compiling Language.Spectacle.Syntax.Enabled.Internal ( src/Language/Spectacle/Syntax/Enabled/Internal.hs, dist/build/Language/Spectacle/Syntax/Enabled/Internal.o, dist/build/Language/Spectacle/Syntax/Enabled/Internal.dyn_o )
[44 of 71] Compiling Language.Spectacle.Syntax.Enabled ( src/Language/Spectacle/Syntax/Enabled.hs, dist/build/Language/Spectacle/Syntax/Enabled.o, dist/build/Language/Spectacle/Syntax/Enabled.dyn_o )
[45 of 71] Compiling Language.Spectacle.Specification.Variable ( src/Language/Spectacle/Specification/Variable.hs, dist/build/Language/Spectacle/Specification/Variable.o, dist/build/Language/Spectacle/Specification/Variable.dyn_o )
[46 of 71] Compiling Language.Spectacle.Syntax.Plain.Internal ( src/Language/Spectacle/Syntax/Plain/Internal.hs, dist/build/Language/Spectacle/Syntax/Plain/Internal.o, dist/build/Language/Spectacle/Syntax/Plain/Internal.dyn_o )
[47 of 71] Compiling Language.Spectacle.Syntax.Plain ( src/Language/Spectacle/Syntax/Plain.hs, dist/build/Language/Spectacle/Syntax/Plain.o, dist/build/Language/Spectacle/Syntax/Plain.dyn_o )
[48 of 71] Compiling Language.Spectacle.Syntax.Prime.Internal ( src/Language/Spectacle/Syntax/Prime/Internal.hs, dist/build/Language/Spectacle/Syntax/Prime/Internal.o, dist/build/Language/Spectacle/Syntax/Prime/Internal.dyn_o )
[49 of 71] Compiling Language.Spectacle.RTS.Registers ( src/Language/Spectacle/RTS/Registers.hs, dist/build/Language/Spectacle/RTS/Registers.o, dist/build/Language/Spectacle/RTS/Registers.dyn_o )
[50 of 71] Compiling Language.Spectacle.Syntax.Env.Internal ( src/Language/Spectacle/Syntax/Env/Internal.hs, dist/build/Language/Spectacle/Syntax/Env/Internal.o, dist/build/Language/Spectacle/Syntax/Env/Internal.dyn_o )
[51 of 71] Compiling Language.Spectacle.Syntax.Env ( src/Language/Spectacle/Syntax/Env.hs, dist/build/Language/Spectacle/Syntax/Env.o, dist/build/Language/Spectacle/Syntax/Env.dyn_o )
[52 of 71] Compiling Language.Spectacle.Syntax.Prime ( src/Language/Spectacle/Syntax/Prime.hs, dist/build/Language/Spectacle/Syntax/Prime.o, dist/build/Language/Spectacle/Syntax/Prime.dyn_o )
[53 of 71] Compiling Language.Spectacle.AST.Temporal ( src/Language/Spectacle/AST/Temporal.hs, dist/build/Language/Spectacle/AST/Temporal.o, dist/build/Language/Spectacle/AST/Temporal.dyn_o )
[54 of 71] Compiling Language.Spectacle.Specification.Prop ( src/Language/Spectacle/Specification/Prop.hs, dist/build/Language/Spectacle/Specification/Prop.o, dist/build/Language/Spectacle/Specification/Prop.dyn_o )
[55 of 71] Compiling Language.Spectacle.Model.ModelError ( src/Language/Spectacle/Model/ModelError.hs, dist/build/Language/Spectacle/Model/ModelError.o, dist/build/Language/Spectacle/Model/ModelError.dyn_o )
[56 of 71] Compiling Language.Spectacle.Model.ModelTemporal ( src/Language/Spectacle/Model/ModelTemporal.hs, dist/build/Language/Spectacle/Model/ModelTemporal.o, dist/build/Language/Spectacle/Model/ModelTemporal.dyn_o )
[57 of 71] Compiling Language.Spectacle.Syntax.Closure.Internal ( src/Language/Spectacle/Syntax/Closure/Internal.hs, dist/build/Language/Spectacle/Syntax/Closure/Internal.o, dist/build/Language/Spectacle/Syntax/Closure/Internal.dyn_o )
[58 of 71] Compiling Language.Spectacle.Syntax.Closure ( src/Language/Spectacle/Syntax/Closure.hs, dist/build/Language/Spectacle/Syntax/Closure.o, dist/build/Language/Spectacle/Syntax/Closure.dyn_o )
[59 of 71] Compiling Language.Spectacle.Syntax.Quantifier.Internal ( src/Language/Spectacle/Syntax/Quantifier/Internal.hs, dist/build/Language/Spectacle/Syntax/Quantifier/Internal.o, dist/build/Language/Spectacle/Syntax/Quantifier/Internal.dyn_o )
[60 of 71] Compiling Language.Spectacle.Syntax.Quantifier ( src/Language/Spectacle/Syntax/Quantifier.hs, dist/build/Language/Spectacle/Syntax/Quantifier.o, dist/build/Language/Spectacle/Syntax/Quantifier.dyn_o )
[61 of 71] Compiling Language.Spectacle.Syntax ( src/Language/Spectacle/Syntax.hs, dist/build/Language/Spectacle/Syntax.o, dist/build/Language/Spectacle/Syntax.dyn_o )
[62 of 71] Compiling Language.Spectacle.AST.Action ( src/Language/Spectacle/AST/Action.hs, dist/build/Language/Spectacle/AST/Action.o, dist/build/Language/Spectacle/AST/Action.dyn_o )
[67 of 71] Compiling Language.Spectacle.AST ( src/Language/Spectacle/AST.hs, dist/build/Language/Spectacle/AST.o, dist/build/Language/Spectacle/AST.dyn_o )
[68 of 71] Compiling Language.Spectacle.Model.ModelAction ( src/Language/Spectacle/Model/ModelAction.hs, dist/build/Language/Spectacle/Model/ModelAction.o, dist/build/Language/Spectacle/Model/ModelAction.dyn_o )

Seems like the 9.0 syntax / type checking changes.

Fix the spanning tree spec for spectacle-1.0.0

The spanning tree spec was disabled for spectacle-1.0.0 and we forgot to update it for 1.0.0 and re-enable it.

Print States Leading Up To Error

Is there a way to print the complete list of state transitions leading to an error state like this?

How to disable a formula?

In TLA+, I can disable a formula by giving a conjunction like so:

Action ==
    /\  state = 0
    /\  state' = 1

Here, Action is only enabled when state is 0. How can I express this in Spectacle? Do I return False from an action? A minimal example would be nice.

Generating counterexample behaviors with Interaction seems awkward?

Consider the DieHard example, but this goes for anything: a normal run yields

specification: model check: failure
refuted property: always "isSolved"
  * from: 0x5da6be4b
      #smallJug = 3
      #bigJug = 1
  * to: 0x9ef6be4b
      #smallJug = 0
      #bigJug = 4

This is a perfectly sensible counterexample, but the thing is, I generally don't want the inviolate state; it's the very temporal specification itself, so it's apparent. Instead, I want the behavior resulting in this state so that I can understand how it lead here. The specific use case is CI to record bad traces, but even in normal dev cycles, I'd want this.

So normally I would now run ./Spec.hs -tl and then look through the trace diagram for the ending state, then follow the trace backwards to the root. But why can't this simply be emitted immediately? Am I missing something? I don't think I've seen this functionality anywhere.

Part of it is that the API isn't quite set up for this just yet it seems. modelcheck fundamentally doesn't allow you to access the resulting Tree World trace; its type either gives you a Left Error for a counterexample or Right (Tree World) for a successful trace. So if there is a temporal violation then you can't even get the traces.

So in the above case you'd have to modelcheck, and in the case of an error re-modeltrace and look for the resulting inviolate state in the Tree and track the states leading there with a search. This seems suboptimal, but doable. Alternatively, you could modeltrace from the start and simply look for any inviolate state according to the temporal property, but this seems like a delicate thing the API should handle for you? And it seems like there's probably a reason they're separate APIs, for now.

But ultimately I just want a counterexample behavior. So if I have to modelcheck-then-modeltrace, I suppose that's fine, but this feels like something that should be handled natively. And this will certainly require a big API change between the two I'd think. Honestly, it feels like there should only be one API entry point with an abstract options record we could configure the model checker with to get these results, but this ticket is probably long enough for now and capable of starting a discussion.¹

I actually think Spectacle being API driven from Haskell is an absolutely massive advantage over something like TLA⁺ that isn't stressed enough, since it allows a lot of integration flexibility that TLA+ doesn't; for example generating HTML reports from counterexample traces for use in CI is my final goal, and that's just going to be massively easier. Model-based test case generation would be another good example. ↩

Weird behaviour with NonDet and Stays modality

Smallest reproduction I could build:

module Specs.ConvergenceSpec where

import Control.Monad (guard)
import Data.Either qualified as Either
import Data.Type.Rec (RecF)
import Language.Spectacle
import Test.Hspec (Spec, hspec, it, shouldSatisfy)

main :: IO ()
main = hspec spec

initialStepsLeft :: Word
initialStepsLeft = 4

spec :: Spec
spec = do
  it "model checks specification with stepNegative and stepPositive actions" $ do
    result <-
      modelcheck
        ( specification $
            ConF #stepNegative (takeStep (pure pred)) $
              ConF #stepPositive (takeStep (pure succ)) NilF
        )
    result `shouldSatisfy` Either.isRight
  it "model checks specification with a single takeStep action that can go negative or positive" $ do
    result <-
      modelcheck
        ( specification $
            ConF #takeStep (takeStep (oneOf [pred, succ])) NilF
        )
    result `shouldSatisfy` Either.isRight

specification ::
  RecF (ActionType '["stepsLeft" # Word, "position" # Int]) acts ->
  Specification
    '["stepsLeft" # Word, "position" # Int]
    acts
    '["staysAtZero" # 'Stays]
specification specNext =
  Specification
    { specInit =
        ConF #stepsLeft (pure initialStepsLeft) $
          ConF #position (pure 0) NilF
    , specNext = specNext
    , specProp =
        ConF #staysAtZero atZero NilF
    }

takeStep ::
  Action '["stepsLeft" # Word, "position" # Int] (Int -> Int) ->
  ActionType '["stepsLeft" # Word, "position" # Int] 'WeakFair
takeStep possibleSteps = ActionWF do
  stepsLeft <- plain #stepsLeft
  guard (stepsLeft > 0)
  position <- plain #position
  delta <- possibleSteps
  let newPosition = delta position
  guard (abs newPosition < fromIntegral stepsLeft) -- never go so far that we can't come back
  #position .= pure newPosition
  #stepsLeft .= pure (pred stepsLeft)
  pure True

atZero :: TemporalType '["stepsLeft" # Word, "position" # Int] 'Stays
atZero = PropFG $ ((0 :: Int) ==) <$> plain #position

The spec models a behaviour where we start at 0, there are a finite number of steps to be taken, and we never take a step away from 0 if it would take us to a distance that is too far to go back. We should be able to move around, but eventually, we should end up stuck at position == 0 (with either 1 or 0 steps left, depending on whether the initial number of steps is odd or even).

In the first test case, we have two possible actions: stepNegative tries to decrease the position, stepPositive tries to increase the position. In the second test case, we have a single action takeStep that uses oneOf to decide whether to decrease or increase the position.

I would expect both cases to be equivalent,. However, the first test case passes, while the second fails.

For some reason, I'm only able to reproduce if initialStepsLeft is >= 4.

Checking Inductive Invariants

I am not entirely familiar with the implementation of the model checker in spectacle, but I am assuming that it is a haskell implementation of TLC. I was wondering if it would be possible to implement something like apalache for the spectacle checker. My understanding is that they convert parts of a TLA spec to constraints that can be interpreted by an SMT solver, and can therefore handle things like unbounded integers or really large sets.

I am mostly asking this question out of curiosity. I wish I understood apalache well enough to offer a contribution (maybe one day). Some of the reasons I think this would be a good fit:

Haskell has a rich SMT library
Part of the Apalache program is providing a type checker for specs, which seems to be a goal of this project as well
I think the eDSL approach lends itself well to this kind of extension

Rename type ascription syntax

Theres a good point in #11 saying that using (#) in the row of a Rec for type ascription is an unconventional choice and should be replaced with something more like haskells ascription syntax such as (:::) or (.::). This would also make things consistent with the (.|) constraint.

Publish a new revision of `spectacle-1.0.0` to remove the changelog entry

Since we're now at version 1.0.0, the changelog entries should be reserved for any versions released after this version.

Temporal formula not applied to initial states

The model checker does not apply a specifications temporal formula to initial states. A minimal example of the issue is:

type Spec = '[]

specInit :: Initial Spec ()
specInit = return ()

specNext :: Action Spec Bool
specNext = return True

specProp :: Invariant Spec Bool
specProp = always (return False)

checkSpec :: Either [MCError Spec] ModelMetrics
checkSpec = modelCheck (Specification specInit specNext specProp Nothing unfair)

The expected behavior from running checkSpec would be that the always (return False) invariant was violated; however, the actual behavior is that the model checking terminates successfully after generating the initial states.

Stuttering steps are not inserted for unchanged steps

The current algorithm for checking the "eventually" modality has unexpected failures for specifications with next actions that do not make progress. If a specification does not explicitly assign the new values for the specification state using the prime operation, the model checker will not insert a stutter-step. The failure to introduce a stutter-step can cause the eventually checker to refute valid specifications.

Minimal Example

Considering the following specification:

type AlphabetVars = '["letter" # Char]

type AlphabetSpec = Specification AlphabetVars '["next" # 'WeakFair] '["isLetterZ" # 'Eventually]

isLetterZ :: Temporal AlphabetVars Bool
isLetterZ = do
  clock <- plain #letter
  pure (clock == 'z')

bitClockSpec :: AlphabetSpec
bitClockSpec =
  Specification
    { specInit = ConF #letter (pure 'a') NilF
    , specNext = ConF #next (ActionWF next) NilF
    , specProp = ConF #isLetterZ (PropF isLetterZ) NilF
    }

If we define the next function to be:

next :: Action AlphabetVars Bool
next = do
  letter <- plain #letter
  #letter .= pure (succ letter)
  pure (letter < 'z')

The model checker is able to find evidence that satisfies the proposition "eventually, the unprimed value of letter will be equal to the character 'z'". This is due to the final stutter-step satisfying plain #letter == 'z', which can be seen in the trace:

$ cabal v2-repl integration-tests
ghci> import Specifications.Alphabet
ghci> :set args --trace --diagram
ghci> alphabetSpecInteract
* 0x5a7b1068
│   #letter = 'z'
│ 
* 0x5a7b1068
│   #letter = 'z'
│ 
* 0x6a7b1068
│   #letter = 'y'
│ 
... 
│ 
* 0xdb7b1068
│   #letter = 'b'
│ 
* 0xeb7b1068
    #letter = 'a'

check(pass)+trace

However, if next is reformulated such that #letter .= pure (succ letter) is only evaluated conditionally, then the resulting trace no longer contains the stutter-step satisfying plain #letter == 'z'. For example, the following definition of next:

next :: Action AlphabetVars Bool
next = do
  letter <- plain #letter
  when (letter < 'z') do
    #letter .= pure (succ letter)
  pure True

Should be equivalent to the former definition. However, wrapping(.=) with a when guard produces the following trace:

$ cabal v2-repl integration-tests
ghci> import Specifications.Alphabet
ghci> :set args --trace --diagram
ghci> alphabetSpecInteract
refuted property: eventually "isLetterZ"
  * from: 0x5a7b1068
      #letter = 'z'
  * to: 0x6a7b1068
      #letter = 'y'

* 0x5a7b1068
│   #letter = 'z'
│ 
* 0x6a7b1068
│   #letter = 'y'
│ 
...
│ 
* 0xdb7b1068
│   #letter = 'b'
│ 
* 0xeb7b1068
    #letter = 'a'

check(fail)+trace

Detect liveness violations in infinite unchanging extensions

Liveness property violations are not checked when an infinite extension of unchanging worlds is appended to a weakly fair process. This leads to an eventually qualified formula appearing true so long as a suffix is unchanged, even if the liveness property hasn't yet been satisfied along the execution trace.

A minimal example:

type CyclicLivenessSpec =
  '[ "x" # Int
   , "s" # Bool
   ]

specInit :: Initial CyclicLivenessSpec ()
specInit = do
  #x `define` return 0
  #s `define` return True

specNext :: Action CyclicLivenessSpec ()
specNext = do 
  s <- plain #s 
  when s do
    x <- plain #x 
    if x == 2 
      then do 
        #x .= return 1 -- Should violate specProp
        #s .= return False 
      else #x .= return (x + 1)  
  return True
    
specProp :: Invariant CyclicLivenessSpec Bool
specProp = eventually do
  s <- plain #s
  x <- plain #x
  x' <- prime #x
  return (x == 2 && x' == 0)

specProp expects some action to occur where x = 2 && x' = 0, but because specNext sets x' = 1 when x = 2, we would expect specProp to emit an error. Because s' = False when x = 2 and all variables are unchanged when #s is false, the sequence repeats with (x = 1 && s = False) infinitely and the model checker accepts this specification as correct.

Model checker option to emit state trace.

Add an option to the model checker for emitting execution traces.