0226b74305
fix tests
2023-02-13 16:47:22 -05:00
1607f7df45
fix info.rkt
2023-02-10 16:55:59 -05:00
e9703a4189
make Observe* more flexible
2023-02-10 16:46:11 -05:00
a0e8b59299
make Int a union type of Zero and NonZero
2023-02-10 16:46:11 -05:00
042d667311
improve handling of initial field type for var asserts
2023-02-10 16:46:11 -05:00
2f17f77d31
add define-ltl
2023-02-10 16:46:11 -05:00
b273586616
small var assert example working with spin
2023-02-10 16:46:11 -05:00
26f15564f1
wip on addying var asserts to SPIN
2023-02-10 16:46:11 -05:00
3801174525
add WritesField effect
2023-02-10 16:46:11 -05:00
4ab405fd70
minimal VarAssert in turnstile working
2023-02-10 16:46:11 -05:00
e514453a12
start on type-varying asserts
2023-02-10 16:46:11 -05:00
c78cf5bb3d
define := and ! for writing/reading fields
2023-02-10 16:46:11 -05:00
59042f9180
test case
2023-02-10 16:46:11 -05:00
28b8bf742f
gitignore
2023-02-10 16:46:11 -05:00
4808004d64
consolidate effect checking to a single key
2023-02-10 16:46:11 -05:00
45425eb68d
Make True and False types, and Bool an alias for the union
2023-02-10 16:46:11 -05:00
2064bd8f00
clarify execution order
2023-02-10 16:46:11 -05:00
6a7879c06e
library function on maybe values
2023-02-10 16:46:11 -05:00
643cc4d3ab
allow type annotation on query-values
2023-02-10 16:46:11 -05:00
e4ca56a002
fix bug in polymorphic defns I introduced
2023-02-10 16:46:11 -05:00
8af4464443
working version of with-facets
2023-02-10 16:46:11 -05:00
0d839cbb12
wip on with-facets
2023-02-10 16:46:11 -05:00
7a50ed2f5e
wip on with-facets
2023-02-10 16:46:11 -05:00
899fe287b4
update uses of auxiliary-macro-context
2023-02-10 16:45:04 -05:00
3d9b1c383c
typed: update info.rkt
2022-07-19 09:32:10 -04:00
7f54c4ccd0
typed: start a SPIN test suite
2022-07-07 12:02:25 -04:00
43cc25ea1b
typed: model checking improvements
2022-06-17 15:59:20 -04:00
798e66dc8c
typed: add turns to spin model
2022-06-13 14:50:17 -04:00
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
b8d580faf3
typed: add release LTL operator
2022-06-13 14:38:12 -04:00
28e89297f9
typed: fix redundancy in RoleNTimes
2022-06-13 14:33:52 -04:00
a5e6caaa52
fix RoleNTimes
2022-06-03 15:40:17 -04:00
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
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
e42460b5e6
typed: improve regex for spin output
2022-06-01 13:47:26 -04:00
788c9b0e46
typed: change compile flags for spin models to allow more processes
2022-06-01 13:46:31 -04:00
c9b25df034
typed: improvements and bug fixes for eliding type annotations
2022-05-04 21:00:31 -04:00
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
d2e753d303
typed: bug fix
2022-04-04 10:16:10 -04:00
29b1171aa8
typed: better support for messages in spin traces
2022-04-01 12:38:01 -04:00
fc038877f5
typed: fix required struct type constructors to know their arity
2022-03-23 12:27:03 -04:00
e4f72519f0
typed: fix type error in tcp driver
2022-03-23 11:55:05 -04:00
2327648499
typed: fiddle with SPIN frontend error
2022-03-23 11:54:17 -04:00
6985022a4b
typed: improve spin-related output and reporting
2022-03-23 11:49:48 -04:00
ce965d9025
typed: add missing file
2022-03-22 15:47:44 -04:00
384d0dbdc1
typed: allow struct imports in require/typed
2022-03-16 13:07:23 -04:00
06aa3690c7
typed: introduce default naming convention for constructor types
2022-03-16 12:04:50 -04:00
6058330961
typed: convenience constructor for subscription types, Observe★
2022-03-16 11:25:07 -04:00
fe798f72a1
untyped: omit a test that the package server does not like
2022-03-07 15:03:43 -05:00
f5f15a5728
typed: handle types in spec that aren't explicit in program
2022-03-07 12:39:58 -05:00
Sam Caldwell