TLA2B operation identifier clash

[leuschel]

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.

• [x] show position information
• [ ] don't create an AST with two operations having the same name

[cobizobi]

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.