search

DistCompiler / pgo

PGo is a source to source compiler from Modular PlusCal specs into Go programs.
https://distcompiler.github.io/
Apache License 2.0
174 stars 14 forks source link

PGo succeeds but outputs empty translation #115

Closed blueish closed 5 years ago

blueish commented 5 years ago

PGo Version: 0.1.4

Input MPCal: https://gist.github.com/blueish/162ec192af87bb859990168b84139f21 Command run: 

blue@bravo:~/dev/538b/a2$ java -jar ~/dev/tla/pgo-v0.1.4.jar -m ./replicated_kv.tla 
Feb 25, 2019 3:32:45 PM pgo.PGoMain run
INFO: Opening source file
Feb 25, 2019 3:32:45 PM pgo.PGoMain run
INFO: Parsing modular PlusCal code
Feb 25, 2019 3:32:47 PM pgo.PGoMain run
INFO: Parsing TLA+ module
Feb 25, 2019 3:32:49 PM pgo.PGoMain validateSemantics
INFO: Validating Modular PlusCal semantics
Feb 25, 2019 3:32:49 PM pgo.PGoMain expandPlusCalMacros
INFO: Expanding PlusCal macros
Feb 25, 2019 3:32:49 PM pgo.PGoMain resolveScopes
INFO: Resolving scopes
Feb 25, 2019 3:32:49 PM pgo.PGoMain mpcalCompilePipeline
INFO: Generating PlusCal code
Feb 25, 2019 3:32:49 PM pgo.PGoMain main
INFO: Finished

Output seems to be empty, and attempting to translate the file in TLA+ toolbox results in an error:

image

minhnhdo commented 5 years ago

Thanks for the report.

The reason for the empty algorithm block is that your MPCal spec does not have an instance statement. You should add something like process (P = 0) == instance Put(arguments...), replacing arguments... with correct arguments to get some output.