Re: [tlaplus] TLA+ Prover Error

[Martin <martin...@xxxxxxxxxxxxxx>]

Hello Reza,

It seems you have not installed the TLA proof system or it is not
available in your $PATH variable. Just as a small explanation: TLA
specifications can be checked with the TLC model checker included in the
toolbox, but you can also write proofs for theorems on specifications
and check them with TLAPS which is distributed seperately[1]. As Stephan
already mentioned, it might be easier to first learn how to write
specifications before you prove properties about them.

Leslie provides excellent material with the Hyperbook and the extensive
"Specifying Systems" on his homepage[2], even including a series of
video lectures. Recently, Ron wrote a series of blog postings with an
introduction to TLA and Hillel created a tutorial[4]. For more material,
just browse the google group :)

I hope you have fun discovering TLA,
cheers Martin


[1] https://tla.msr-inria.inria.fr/tlaps/content/Home.html
[2] https://lamport.azurewebsites.net/tla/tla.html
[3] https://pron.github.io/posts/tlaplus_part1
[4] https://learntla.com/introduction/

On 07/19/2017 10:57 AM, reza parvizi wrote:
> 'Prover Launch' has encountered a problem.
> 
> The following error occurred while running the PM :
> Cannot run program "tlapm" (in directory " C:\Users\Pahmadr\Documents"): CreateProcess error=2, The system cannot find the file specified
>