awakesecurity / spectacle

Embedded specification language & model checker in Haskell
Apache License 2.0
175 stars 12 forks source link

Syntax/error #7

Closed riz0id closed 3 years ago

riz0id commented 3 years ago

This PR adds in the Error effect, which implements throw/catch using the new higher-order interface. Error is used by the temporal operations and logical quantifiers to report failures to the model checker.