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.

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

TLA2B operation identifier clash #366

Open
1 of 2 tasks
leuschel opened this issue Sep 24, 2024 · 1 comment
Open
1 of 2 tasks

TLA2B operation identifier clash #366

leuschel opened this issue Sep 24, 2024 · 1 comment
Labels
bug Something isn't working TLA2B TLA to B Translation

Comments

@leuschel
Copy link
Member

leuschel commented Sep 24, 2024

If a TLA+ next state uses a definition twice, then TLA2B will create an AST with two operations having the same name, leading to errors when type checking the AST.
An example which exhibits is here: public_examples/TLA/pilot-tla/pilot/MC.tla
taken from
https://github.com/raulpardo/pilot-tla/blob/master/pilot.toolbox/pilot_correctness/pilot.tla
where we have

Next == \E dc1,dc2 \in DCs : 
            \E p \in Policies :
                \E ds \in DSs : 
                    \/ Choose_policy(dc1,p)
                    \/ Choose_policy(ds,p)
                    \/ Request_collection(dc1,ds,p)
                    \/ Request_transfer(dc1,dc2,p)
                    \/ Send1(ds,dc1,p)
                    \/ Transfer1(dc1,dc2,p)

leading to the error
Operation identifier 'Choose_policy' (local from MC) already declared at (local from MC)
Also note that the operations seem to have no position information in the generated AST.

  • show position information
  • don't create an AST with two operations having the same name
@leuschel leuschel added bug Something isn't working TLA2B TLA to B Translation labels Sep 24, 2024
@cobizobi
Copy link

The position information should now be available, both in Tcl/Tk and in ProB2-UI and including the correct file path. The position information of TLA2B was not available in ProB2 because the PositionPrinter in the RecursiveMachineLoader was not set correctly.

@iTitus iTitus closed this as completed Oct 25, 2024
@cobizobi cobizobi reopened this Oct 26, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working TLA2B TLA to B Translation
Projects
None yet
Development

No branches or pull requests

3 participants