Re: [tlaplus] Error : Taking snapshot of Model

[Markus Kuppe <tlaplus-go...@xxxxxxxxxxx>]

On 03.10.2018 21:00, yashmeh...@xxxxxxxxx wrote:
> Hello, I am getting this error when I am trying to run my model.
> An internal error occurred during: "Taking snapshot of Model_3...".
> Attempted to beginRule: F/LamportMutex/LamportOrig.toolbox, does not match outer scope rule: P/LamportOrig
> 
> Can someone Help me with this error?

Hi,

can you please open up a bug report at
https://github.com/tlaplus/tlaplus/issues and provide as much detail as
possible.  Ideally, attach the content of the .log file. The   .log
file is in the   .tlaplus/.metadata/ folder in your home directory.  On
Windows, you can find out where your home directory is located, by by
entering the command echo %SYSTEMDRIVE%%HOMEPATH% in Command Prompt.  On
Linux and Mac, check the $HOME variable.

Thanks
Markus