pgo

pgo copied to clipboard

Currently, most systems are in the `test/files/general/` and some of them are in the `benchmark/` folder. I think the large systems are not test cases anymore and they should have...

shayanh

Currently, this is the persistent resource interface: ```go type PersistableResource interface { distsys.ArchetypeResource GetState() ([]byte, error) } ``` And it just supports persisting the state. Reading and recovery from the...

shayanh

Support TLA+ 2

1

So far, PGo has been developed blissfully ignorant of TLA+ 2, and it had not caused problems. When discussing how to implement the sum of a set of integers, however,...

fhackett

Suggestion to improve readability of the compiled Go code

4

I suggest changing API of `Read` and `Write` methods of `ArchetypeInterface`. Current API: ```go func (iface ArchetypeInterface) Write(handle ArchetypeResourceHandle, indices []tla.TLAValue, value tla.TLAValue) (err error) func (iface ArchetypeInterface) Read(handle ArchetypeResourceHandle,...

shayanh

TLA+ module support (for completeness)

2

Currently, PGo will crash with `NotImplementedError` if a TLA+ module it's compiling references external definitions. Anything involving `EXTENDS`, `INSTANCE` and a module that is not built-in will cause this problem....

fhackett

Accepting labels as macros' arguments

1

PlusCal and MPCal don't accept labels as macros' arguments. Input labels in macros can be used in `goto` statements. For example, by having this we can define the following macro,...

shayanh

Documentation outdated

1

https://github.com/UBC-NSS/pgo/blob/master/manual.pdf still mentions ant but the build has apparently been migrated to gradle.

lemmy

Generated Code Conformance Checking

3

Related to #122, this is an idea about how to verify that PGo-generated code actually does what the model says it does. Key idea: encoded into an MPCal model, there...

fhackett

Compiler validation: provide an option for PGo to attempt compiling invariants into generated code

5

It would be much easier to argue PGo's soundness, if generated programs could check themselves. This issue suggests adding a flag to PGo, such that it attempts to extract safety...

fhackett

```tla archetype A(ref network) { a: network[LEADER] := [type |-> HELLO, messages |-> [log |-> ]]; } ``` An archetype like defined above leads messages failing to be sent across...

rmascarenhas