Sam Caldwell
e9703a4189
make Observe* more flexible
2023-02-10 16:46:11 -05:00
Sam Caldwell
a0e8b59299
make Int a union type of Zero and NonZero
2023-02-10 16:46:11 -05:00
Sam Caldwell
042d667311
improve handling of initial field type for var asserts
2023-02-10 16:46:11 -05:00
Sam Caldwell
2f17f77d31
add define-ltl
2023-02-10 16:46:11 -05:00
Sam Caldwell
b273586616
small var assert example working with spin
2023-02-10 16:46:11 -05:00
Sam Caldwell
26f15564f1
wip on addying var asserts to SPIN
2023-02-10 16:46:11 -05:00
Sam Caldwell
3801174525
add WritesField effect
2023-02-10 16:46:11 -05:00
Sam Caldwell
4ab405fd70
minimal VarAssert in turnstile working
2023-02-10 16:46:11 -05:00
Sam Caldwell
e514453a12
start on type-varying asserts
2023-02-10 16:46:11 -05:00
Sam Caldwell
c78cf5bb3d
define := and ! for writing/reading fields
2023-02-10 16:46:11 -05:00
Sam Caldwell
59042f9180
test case
2023-02-10 16:46:11 -05:00
Sam Caldwell
28b8bf742f
gitignore
2023-02-10 16:46:11 -05:00
Sam Caldwell
4808004d64
consolidate effect checking to a single key
2023-02-10 16:46:11 -05:00
Sam Caldwell
45425eb68d
Make True and False types, and Bool an alias for the union
2023-02-10 16:46:11 -05:00
Sam Caldwell
2064bd8f00
clarify execution order
2023-02-10 16:46:11 -05:00
Sam Caldwell
6a7879c06e
library function on maybe values
2023-02-10 16:46:11 -05:00
Sam Caldwell
643cc4d3ab
allow type annotation on query-values
2023-02-10 16:46:11 -05:00
Sam Caldwell
e4ca56a002
fix bug in polymorphic defns I introduced
2023-02-10 16:46:11 -05:00
Sam Caldwell
8af4464443
working version of with-facets
2023-02-10 16:46:11 -05:00
Sam Caldwell
0d839cbb12
wip on with-facets
2023-02-10 16:46:11 -05:00
Sam Caldwell
7a50ed2f5e
wip on with-facets
2023-02-10 16:46:11 -05:00
Sam Caldwell
899fe287b4
update uses of auxiliary-macro-context
2023-02-10 16:45:04 -05:00
Sam Caldwell
3d9b1c383c
typed: update info.rkt
2022-07-19 09:32:10 -04:00
Sam Caldwell
7f54c4ccd0
typed: start a SPIN test suite
2022-07-07 12:02:25 -04:00
Sam Caldwell
43cc25ea1b
typed: model checking improvements
2022-06-17 15:59:20 -04:00
Sam Caldwell
798e66dc8c
typed: add turns to spin model
2022-06-13 14:50:17 -04:00
Sam Caldwell
2fb7f4795e
typed: fix performance pathology in role graph compilation
...
Wasn't checking redundancy in adding states to the worklist, so could
end up analyzing the same state many, many times. RoleNTimes exposed
this behavior: going from 3 to 5 repetitions caused compilation to hang
2022-06-13 14:38:42 -04:00
Sam Caldwell
b8d580faf3
typed: add release LTL operator
2022-06-13 14:38:12 -04:00
Sam Caldwell
28e89297f9
typed: fix redundancy in RoleNTimes
2022-06-13 14:33:52 -04:00
Sam Caldwell
a5e6caaa52
fix RoleNTimes
2022-06-03 15:40:17 -04:00
Sam Caldwell
2057a9f5a9
typed: RoleNTimes sugar
...
for setting up (finite) repetitions of behavior to give SPIN,
not exploding state space
2022-06-01 14:38:43 -04:00
Sam Caldwell
3bdace6535
typed: reorder operations when running spin scripts
...
For some reason it was getting stuck on larger spin outputs
2022-06-01 14:36:56 -04:00
Sam Caldwell
e42460b5e6
typed: improve regex for spin output
2022-06-01 13:47:26 -04:00
Sam Caldwell
788c9b0e46
typed: change compile flags for spin models to allow more processes
2022-06-01 13:46:31 -04:00
Sam Caldwell
c9b25df034
typed: improvements and bug fixes for eliding type annotations
2022-05-04 21:00:31 -04:00
Sam Caldwell
b9f655766f
typed: add default types to constructor fields and alternate actor
...
typechecking path
Default types for fields means we can elaborate a binding pattern
without a current communication type.
Then a potential communication type can be the output of type checking
an actor, that is checked when it is instantiated, such as in a
dataspace or other context.
2022-05-03 11:51:06 -04:00
Sam Caldwell
d2e753d303
typed: bug fix
2022-04-04 10:16:10 -04:00
Sam Caldwell
29b1171aa8
typed: better support for messages in spin traces
2022-04-01 12:38:01 -04:00
Sam Caldwell
fc038877f5
typed: fix required struct type constructors to know their arity
2022-03-23 12:27:03 -04:00
Sam Caldwell
e4f72519f0
typed: fix type error in tcp driver
2022-03-23 11:55:05 -04:00
Sam Caldwell
2327648499
typed: fiddle with SPIN frontend error
2022-03-23 11:54:17 -04:00
Sam Caldwell
6985022a4b
typed: improve spin-related output and reporting
2022-03-23 11:49:48 -04:00
Sam Caldwell
ce965d9025
typed: add missing file
2022-03-22 15:47:44 -04:00
Sam Caldwell
384d0dbdc1
typed: allow struct imports in require/typed
2022-03-16 13:07:23 -04:00
Sam Caldwell
06aa3690c7
typed: introduce default naming convention for constructor types
2022-03-16 12:04:50 -04:00
Sam Caldwell
6058330961
typed: convenience constructor for subscription types, Observe★
2022-03-16 11:25:07 -04:00
Sam Caldwell
fe798f72a1
untyped: omit a test that the package server does not like
2022-03-07 15:03:43 -05:00
Sam Caldwell
f5f15a5728
typed: handle types in spec that aren't explicit in program
2022-03-07 12:39:58 -05:00
Sam Caldwell
98b773e7ee
typed: improve dataspace error messages
2022-03-07 12:37:17 -05:00
Sam Caldwell
b4497f1623
typed: add some quasisyntax/loc
2022-03-07 12:33:15 -05:00