[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Error : Taking snapshot of Model
- From: Markus Kuppe <tlaplus-go...@xxxxxxxxxxx>
- Date: Thu, 4 Oct 2018 08:35:36 -0700
- References: <email@example.com>
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?
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.