Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

VeyMont: codegen #1225

Merged
merged 46 commits into from
Aug 9, 2024
Merged

VeyMont: codegen #1225

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
46 commits
Select commit Hold shift + click to select a range
db36b0d
Print Program and Class with whitespaces between declarations
bobismijnnaam Jul 18, 2024
91a828d
Make sure nameless class declarations do not actually count towards h…
bobismijnnaam Jul 18, 2024
62a5fa1
Make sure Predicate is printed with a semicolon. Make warnings from p…
bobismijnnaam Jul 18, 2024
a7a6cfe
Generalize veymont permission generation. Remove old VeyMont flag.
bobismijnnaam Jul 18, 2024
c9a30d2
Whole bunch of changes.
bobismijnnaam Jul 18, 2024
484ef84
Add permission generation for channel field
bobismijnnaam Jul 19, 2024
ffc3c56
Structure the veymont rewrites into verification and generation packa…
bobismijnnaam Jul 19, 2024
52dcada
Finish unfinished refactoring. Refactor VeyMontContext to do more ini…
bobismijnnaam Jul 19, 2024
7ad3a9e
Generate permissions for peer and param fields
bobismijnnaam Jul 19, 2024
cac9f56
Begin on propagating permissions for impl. GenerateImplementation doe…
bobismijnnaam Jul 19, 2024
8ffc0d0
Logging and case study changes.
bobismijnnaam Jul 23, 2024
1a02557
More verbose logging
bobismijnnaam Jul 23, 2024
92a0179
Propagate invariant of committed channels.
bobismijnnaam Jul 23, 2024
821a95d
Include lock invariant proper in wait loop within channels
bobismijnnaam Jul 23, 2024
eefcb05
TTTmsg generated code verifies!
bobismijnnaam Jul 24, 2024
de3a089
Remove some assume falses from TTTlast... Scary!
bobismijnnaam Jul 24, 2024
88131d0
Beef up the pretty printer
bobismijnnaam Jul 24, 2024
063c06c
Encode implication as ternary if
bobismijnnaam Jul 25, 2024
97c9e9b
Good on our way onto encoding globals
bobismijnnaam Jul 25, 2024
6e5a889
Encode global applicables using a statics class
bobismijnnaam Jul 25, 2024
b432226
Running generated code seems to work!
bobismijnnaam Jul 25, 2024
86286fe
Factor out PVL to Java compilation.
bobismijnnaam Jul 30, 2024
c27c42a
Rephrase comments
bobismijnnaam Jul 30, 2024
662fe27
Start integrating VeyMont into test suite.
bobismijnnaam Jul 30, 2024
1d50511
Integrate VeyMont code generation into test suite.
bobismijnnaam Jul 31, 2024
ae75a7a
Fully integrate all case studies into test suite.
bobismijnnaam Jul 31, 2024
f5117f0
Rewrite ExamplesSpec
bobismijnnaam Aug 1, 2024
9ab8718
Continue refactoring VeyMont test suite.
bobismijnnaam Aug 2, 2024
4735b58
HAlfway through refactoring the veymont frontend. Now need to re-impl…
bobismijnnaam Aug 2, 2024
724c76c
Finishing touches for the VeyMont frontend.
bobismijnnaam Aug 6, 2024
15c026c
Make result parsing of test run first class and factor it out. Start …
bobismijnnaam Aug 6, 2024
d73c5f9
Reinstate TechnicalVeyMontSpec.scala
bobismijnnaam Aug 7, 2024
9c77bdb
Generalize or remove todos
bobismijnnaam Aug 7, 2024
66a2fe3
Merge branch 'dev' into veymont-codegen
bobismijnnaam Aug 7, 2024
3532a52
Rewrite part to avoid warning
bobismijnnaam Aug 7, 2024
db603a1
Move case studies to publications folder :)
bobismijnnaam Aug 7, 2024
d87ec78
Remove leftover files from manual encoding
bobismijnnaam Aug 7, 2024
a160151
Add some debug printing
bobismijnnaam Aug 7, 2024
048cb61
Remove $ from runJava class name. It might cause problems in the gith…
bobismijnnaam Aug 7, 2024
95fa125
Ugh. Forgot to change the filename
bobismijnnaam Aug 7, 2024
bc829b6
Invoke javac direclty instead of using (deprecated) javax.tools
bobismijnnaam Aug 7, 2024
8c4477e
Add patcher
bobismijnnaam Aug 8, 2024
a4db7b3
Add patcher as a mode, and not as a run script
bobismijnnaam Aug 8, 2024
80ea25b
Add stages for patcher to avoid bug in Process.scala
bobismijnnaam Aug 8, 2024
f044c5d
Add logtime to veymont
bobismijnnaam Aug 8, 2024
7ab06a8
Rename FM2024 to IFM2024. Clarify generated language for --veymont-ou…
bobismijnnaam Aug 9, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
256 changes: 0 additions & 256 deletions examples/concepts/veymont/FM2024 - VeyMont/1-TTTmsg/TTTmsg-generatedImplementation.pvl
View file
Open in desktop

This file was deleted.

Loading
Loading