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
Sam Caldwell
9952ff9400
omit GL related things from test paths
2022-03-01 12:17:59 -05:00
Sam Caldwell
fd59e58dc3
typed: improve error handling and work around spin front-end limitations
2022-02-25 12:13:52 -05:00
Sam Caldwell
481b490fd2
typed: generate unique end labels in SPIN
2022-02-25 12:04:42 -05:00
Sam Caldwell
3ec1048aad
typed: improve error messages
2022-02-23 11:50:17 -05:00
Sam Caldwell
55477446c2
typed: more string formatting prims
2022-02-23 11:49:55 -05:00
Sam Caldwell
50cac93e1e
bug fix: allow 0-ary structs
2022-02-23 11:49:36 -05:00
Sam Caldwell
fc6e012d1c
fixups to get tests passing
2021-05-10 15:30:46 -04:00
Sam Caldwell
3b75881366
fix type of empty?
2021-05-06 10:10:25 -04:00
Sam Caldwell
690f9e65a8
more docs and cleanups
2021-05-05 12:52:07 -04:00
Sam Caldwell
4f6089c805
more docs and cleanup
2021-05-04 17:15:34 -04:00
Sam Caldwell
aa74ffa14d
remove outdated example
2021-05-04 09:49:21 -04:00
Sam Caldwell
09ce074125
work on typed syndicate docs
2021-05-03 14:59:14 -04:00
Sam Caldwell
3f6a5573e4
Allow importing structs without accessors and opaque external types
2021-04-27 16:51:28 -04:00
Sam Caldwell
98c58d3e6f
Add a typed during/spawn and checks for overly broad interests
2021-04-22 15:38:15 -04:00
Sam Caldwell
c3559f1611
Hide legacy typed/syndicate #lang, consolidate to the "roles" version
2021-04-22 12:09:57 -04:00
Sam Caldwell
8b67d0ba03
test on composing communication types
2021-04-22 11:45:09 -04:00
Sam Caldwell
52e64d6792
move spin scripts
2021-04-22 11:41:31 -04:00
Sam Caldwell
59183b5fe9
reorganize typed syndicate project structure
2021-04-21 10:39:30 -04:00
Sam Caldwell
0191461137
allow importing structs with unknown super-type
2021-04-15 10:54:10 -04:00
Sam Caldwell
6b46be34f9
first draft of verifying messages in spin backend
2021-03-04 11:08:06 -05:00
Sam Caldwell
ff1ac58a36
fix issues with determining stop effects
2021-02-22 11:30:43 -05:00
Sam Caldwell
c54b088a4d
dramatically improve handling of cycles in compile/internal-events
2021-01-28 11:26:11 -05:00
Sam Caldwell
d5894e400b
prototype using syndicate msd logging for displaying spin counterexamples
2021-01-25 11:14:43 -05:00
Sam Caldwell
b023753091
provide an interface for msd tracing
2021-01-25 11:13:12 -05:00
Sam Caldwell
04530893f4
some handling of cycles in spin traces
2021-01-22 10:38:10 -05:00
Sam Caldwell
bd267cfaa9
Translate trail file counterexample back to a syndicate-level trace
2021-01-15 11:15:44 -05:00