issues
search
awakesecurity
/
spectacle
Embedded specification language & model checker in Haskell
Apache License 2.0
175
stars
12
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Stuttering steps are not inserted for unchanged steps
#56
riz0id
opened
1 year ago
0
Enable dual trace and checking mode in CLI
#55
riz0id
closed
1 year ago
0
Documentation + Nix fixes
#54
riz0id
closed
1 year ago
0
Support GHC 9.4.3
#53
NicolasT
closed
1 year ago
1
Various support updates: GHC 9+ support, Flakes, documentation
#52
thoughtpolice
closed
1 year ago
7
Generating counterexample behaviors with Interaction seems awkward?
#51
thoughtpolice
opened
2 years ago
3
Should --only-trace should imply --log when using `interaction`?
#50
thoughtpolice
opened
2 years ago
1
Support GHC 9.0 / base 4.15
#49
sternenseemann
closed
1 year ago
2
Adding "convergence" specification to integration-tests
#48
riz0id
opened
2 years ago
0
Weird behaviour with NonDet and Stays modality
#47
gusbicalho
opened
2 years ago
10
Clear change log
#46
riz0id
opened
2 years ago
0
Updating specifications in integration test suite
#45
riz0id
closed
2 years ago
0
Fix the spanning tree spec for spectacle-1.0.0
#44
ixmatus
closed
2 years ago
0
Publish a new revision of `spectacle-1.0.0` to remove the changelog entry
#43
ixmatus
opened
2 years ago
0
Use `Managed` monad in CLI
#42
riz0id
opened
2 years ago
1
Version bump/1.0.0
#41
riz0id
closed
2 years ago
0
Options parser
#40
riz0id
closed
2 years ago
0
Liveness property checked incorrectly
#39
gusbicalho
closed
2 years ago
1
The integration tests are not verified correctly
#38
y-taka-23
closed
2 years ago
1
Model checker refactor for labelled actions.
#37
riz0id
closed
2 years ago
0
How to disable a formula?
#36
yagehu
closed
3 years ago
1
Temporal Functors
#35
riz0id
closed
3 years ago
5
Checking Inductive Invariants
#34
JonathanLorimer
closed
3 years ago
2
Labelled actions
#33
riz0id
closed
2 years ago
0
Print States Leading Up To Error
#32
JonathanLorimer
closed
2 years ago
1
Adding Spectacle to Hackage & nixpkgs?
#31
byrongibson
closed
2 years ago
3
Detect liveness violations in unchanging infinite sequences
#30
riz0id
closed
3 years ago
0
Detect liveness violations in infinite unchanging extensions
#29
riz0id
closed
3 years ago
0
Apply temporal formula to initial worlds
#28
riz0id
closed
3 years ago
0
Model checker option to emit state trace.
#27
riz0id
closed
2 years ago
0
Temporal formula not applied to initial states
#26
riz0id
closed
3 years ago
0
Model checker exceptions and revised model state representation
#25
riz0id
closed
3 years ago
0
Add a bit clock specification
#24
ixmatus
closed
3 years ago
0
Updated model checker
#23
riz0id
closed
3 years ago
0
Use GitHub Actions matrix syntax
#22
evanrelf
closed
3 years ago
0
Completed Syntax
#21
riz0id
closed
3 years ago
1
Updating the model checker
#20
riz0id
closed
3 years ago
0
Adding unique names to modal operators
#19
riz0id
closed
3 years ago
2
Simplifying Loom
#18
riz0id
closed
3 years ago
0
More Nix simplifications
#17
evanrelf
closed
3 years ago
4
Adding modal operators
#16
riz0id
closed
3 years ago
0
Adding logical operations
#15
riz0id
closed
3 years ago
0
Updating closures
#14
riz0id
closed
3 years ago
0
Updating quantifiers
#13
riz0id
closed
3 years ago
0
Rename type ascription syntax
#12
riz0id
closed
2 years ago
0
Updating primed variables
#11
riz0id
closed
3 years ago
0
Updating plain variables
#10
riz0id
closed
3 years ago
0
Higher-order syntax
#9
riz0id
closed
3 years ago
0
Updating Rec for higher-order effects.
#8
riz0id
closed
3 years ago
0
Syntax/error
#7
riz0id
closed
3 years ago
0
Next