Commit Graph

1472 Commits

Author SHA1 Message Date
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
Sam Caldwell d79378b4a3 clean up generated files 2021-01-11 12:10:05 -05:00
Sam Caldwell 7a8628880a LTL syntax plus form for model checking in typed syndicate 2021-01-11 11:52:00 -05:00
Sam Caldwell 145bc84e33 shell script for running spin 2021-01-11 11:50:50 -05:00
Sam Caldwell 549590d304 missed one 2021-01-11 11:50:05 -05:00
Sam Caldwell cb3f0546c0 notes in Makefile 2021-01-11 11:49:33 -05:00
Sam Caldwell 4e43c489d8 remove unused argument 2021-01-06 12:08:13 -05:00
Sam Caldwell d0f00779cd invoke spin from racket 2021-01-06 11:19:42 -05:00
Sam Caldwell 5a5c651321 Improve simulation checking/failure trace generation
Account for the case where the spec takes a step but the implementation
remains in the same state
2020-12-21 11:07:29 -05:00
Sam Caldwell 1fba368987 Caputre actor actions while booting up a ground dataspace
fixes an issue where a function that evaluates multiple `spawn` forms
only spawns the last actor
2020-12-14 14:22:32 -05:00
Sam Caldwell 7475c1896f stop tracking debugging file 2020-12-14 11:53:52 -05:00
Sam Caldwell 5a90933e9f More work on unit test style simulation checking 2020-12-14 11:50:24 -05:00
Sam Caldwell 8dda1ba6bf Manually assign Type kind to types instead of doing a full
serialize/deserialize

seems to make things as much as 5x faster, and half the code size
2020-12-11 16:40:03 -05:00
Sam Caldwell 45f140d642 add form for writing type to file 2020-12-11 16:40:03 -05:00
Sam Caldwell 95699308dd fix small issue 2020-12-11 16:40:03 -05:00
Sam Caldwell 362e102524 fix constructor resugaring to use the name with the right scopes 2020-12-11 16:40:03 -05:00
Sam Caldwell 78fee55ffa raise an error when pattern elaboration fails to find a real type 2020-12-11 16:40:02 -05:00
Sam Caldwell 2fd3771609 simplify hash impl a little 2020-12-11 16:40:02 -05:00
Sam Caldwell 8be62ed72c work on finding trace counterexample when finding subgraph 2020-12-11 16:40:02 -05:00
Sam Caldwell c9c2d2747b improve some error reporting by moving cuts 2020-12-11 16:40:02 -05:00
Sam Caldwell c20d075d03 fixups to tests 2020-12-11 16:40:02 -05:00
Sam Caldwell 6dd369b08f improvements on verification, nb AnyActor performance hell 2020-12-11 16:40:02 -05:00
Sam Caldwell c9a5af0d10 create lambda shortcut 2020-12-11 16:40:02 -05:00
Sam Caldwell 7d8b62ff02 first draft on finding simulation counterexamples 2020-12-11 16:40:02 -05:00
Sam Caldwell db2a8e1cec fix issues with require-struct accessors 2020-12-11 16:40:02 -05:00
Sam Caldwell 3e13e3e449 work on proto tie-in 2020-12-11 16:40:00 -05:00
Sam Caldwell 8a6931710a create a typed struct out 2020-12-11 16:40:00 -05:00
Sam Caldwell 1805b936be try syntax-local-lift-module-end for lift+define-role 2020-12-11 16:40:00 -05:00
Sam Caldwell 25860019c6 define accessors for require-struct 2020-12-11 16:40:00 -05:00
Sam Caldwell abecc4996c first bit of linking proto analysis into language 2020-12-11 16:40:00 -05:00
Sam Caldwell d523dc7937 define constructor accessors 2020-12-11 16:40:00 -05:00