Re: New to TLA, Can't figure out the example work

[mo jia <life....@xxxxxxxxx>]

I offer the total debug output run in console  by this commond

/usr/local/bin/tlapm --toolbox 0 0 --isaprove -I /usr/local/lib/tlaps/ /home/jiamo/tlaspecs/Euclid/euclid.tla

On Saturday, August 12, 2017 at 10:36:11 PM UTC+8, mo jia wrote:

I am using WSL on windows10.

And some step following https://groups.google.com/forum/#!searchin/tlaplus/%22cvc3%22$20not$20found$20in$20this$20PATH$3A%7Csort:relevance/tlaplus/zrKSDGA9yZ4/UgHm0iLRAwAJ

It work right but not totally right.

The picture is what I have done:

I am following the http://tla.msr-inria.inria.fr/tlaps/content/Documentation/Tutorial/Hierarchical_proofs.html

While I can't figure out why this 

<1>2 Spec => []InductiveInvariant BY PTL, InitProperty, NextProperty, <1>1 DEF Spec

can be proved.

The debug msg in console don't helped me to debug.

Warning: --isaprove is deprecated (ignored)

\* TLAPM version 1.4.3 (commit 34695)
\* launched at 2017-08-12 22:40:08 with command line:
\* /usr/local/bin/tlapm --toolbox 0 0 --isaprove -I /usr/local/lib/tlaps/ /home/jiamo/tlaspecs/Euclid/euclid.tla

(* loading fingerprints in "euclid.tlaps/fingerprints" *)
@!!BEGIN
@!!type:obligation
@!!id:1
@!!loc:37:3:37:5
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:2
@!!loc:37:6:37:22
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:3
@!!loc:63:3:63:5
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:4
@!!loc:63:6:63:10
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:5
@!!loc:63:12:63:16
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:6
@!!loc:63:18:63:22
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:7
@!!loc:46:3:46:10
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:8
@!!loc:49:3:49:10
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:9
@!!loc:54:5:54:7
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:10
@!!loc:54:8:54:12
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:11
@!!loc:54:14:54:18
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:12
@!!loc:54:20:54:32
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:13
@!!loc:52:5:52:7
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:14
@!!loc:52:8:52:12
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:15
@!!loc:61:5:61:7
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:16
@!!loc:61:8:61:12
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:17
@!!loc:61:14:61:18
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:18
@!!loc:61:20:61:24
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:19
@!!loc:61:26:61:38
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:20
@!!loc:57:5:57:7
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:21
@!!loc:57:8:57:12
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:22
@!!loc:59:5:59:7
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:23
@!!loc:59:8:59:12
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:24
@!!loc:59:14:59:18
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:25
@!!loc:59:20:59:32
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:26
@!!loc:73:5:73:7
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:27
@!!loc:73:8:73:11
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:28
@!!loc:73:13:73:17
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:29
@!!loc:73:19:73:23
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:30
@!!loc:67:5:67:7
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:31
@!!loc:69:5:69:7
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:32
@!!loc:69:8:69:11
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:33
@!!loc:69:13:69:25
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:34
@!!loc:69:27:69:39
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:35
@!!loc:69:41:69:45
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:36
@!!loc:71:5:71:7
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligation
@!!id:37
@!!loc:71:8:71:20
@!!status:to be proved
@!!END

@!!BEGIN
@!!type:obligationsnumber
@!!count:37
@!!END

@!!BEGIN
@!!type:obligation
@!!id:1
@!!loc:37:3:37:5
@!!status:proved
@!!prover:smt
@!!meth:time-limit: 5
@!!already:true
@!!END

@!!BEGIN
@!!type:obligation
@!!id:2
@!!loc:37:6:37:22
@!!status:trivial
@!!prover:tlapm
@!!already:false
@!!END

@!!BEGIN
@!!type:obligation
@!!id:3
@!!loc:63:3:63:5
@!!status:proved
@!!prover:smt
@!!meth:time-limit: 5
@!!already:true
@!!END

@!!BEGIN
@!!type:obligation
@!!id:4
@!!loc:63:6:63:10
@!!status:trivial
@!!prover:tlapm
@!!already:false
@!!END

@!!BEGIN
@!!type:obligation
@!!id:5
@!!loc:63:12:63:16
@!!status:trivial
@!!prover:tlapm
@!!already:false
@!!END

@!!BEGIN
@!!type:obligation
@!!id:6
@!!loc:63:18:63:22
@!!status:trivial
@!!prover:tlapm
@!!already:false
@!!END

@!!BEGIN
@!!type:obligation
@!!id:7
@!!loc:46:3:46:10
@!!status:proved
@!!prover:smt
@!!meth:time-limit: 5
@!!already:true
@!!END

@!!BEGIN
@!!type:obligation
@!!id:8
@!!loc:49:3:49:10
@!!status:proved
@!!prover:smt
@!!meth:time-limit: 5
@!!already:true
@!!END

@!!BEGIN
@!!type:obligation
@!!id:9
@!!loc:54:5:54:7
@!!status:failed
@!!prover:smt
@!!meth:time-limit: 5
@!!reason:false
@!!already:true
@!!obl:ASSUME NEW CONSTANT M,
       NEW CONSTANT N,
       NEW VARIABLE x,
       NEW VARIABLE y,
       /\ x \in Number
       /\ y \in Number
       /\ GCD(x, y) = GCD(M, N) ,
       \/ /\ x < y
          /\ y' = y - x
          /\ x' = x
       \/ /\ y < x
          /\ x' = x - y
          /\ y' = y ,
       x < y ,
       y - x \in Number /\ ~y < x ,
       \A p, q \in Number : p < q => GCD(p, q) = GCD(p, q - p) 
PROVE  (/\ x \in Number
        /\ y \in Number
        /\ GCD(x, y) = GCD(M, N))'

@!!END

@!!BEGIN
@!!type:obligation
@!!id:9
@!!loc:54:5:54:7
@!!status:proved
@!!prover:zenon
@!!meth:time-limit: 10
@!!already:true
@!!END

@!!BEGIN
@!!type:obligation
@!!id:10
@!!loc:54:8:54:12
@!!status:trivial
@!!prover:tlapm
@!!already:false
@!!END

@!!BEGIN
@!!type:obligation
@!!id:11
@!!loc:54:14:54:18
@!!status:trivial
@!!prover:tlapm
@!!already:false
@!!END

@!!BEGIN
@!!type:obligation
@!!id:12
@!!loc:54:20:54:32
@!!status:trivial
@!!prover:tlapm
@!!already:false
@!!END

@!!BEGIN
@!!type:obligation
@!!id:13
@!!loc:52:5:52:7
@!!status:proved
@!!prover:smt
@!!meth:time-limit: 5
@!!already:true
@!!END

@!!BEGIN
@!!type:obligation
@!!id:14
@!!loc:52:8:52:12
@!!status:trivial
@!!prover:tlapm
@!!already:false
@!!END

@!!BEGIN
@!!type:obligation
@!!id:15
@!!loc:61:5:61:7
@!!status:failed
@!!prover:smt
@!!meth:time-limit: 5
@!!reason:false
@!!already:true
@!!obl:ASSUME NEW CONSTANT M,
       NEW CONSTANT N,
       NEW VARIABLE x,
       NEW VARIABLE y,
       /\ x \in Number
       /\ y \in Number
       /\ GCD(x, y) = GCD(M, N) ,
       \/ /\ x < y
          /\ y' = y - x
          /\ x' = x
       \/ /\ y < x
          /\ x' = x - y
          /\ y' = y ,
       y < x ,
       x - y \in Number /\ ~x < y ,
       GCD(y', x') = GCD(y, x) ,
       \A p, q \in Number : GCD(p, q) = GCD(q, p) 
PROVE  (/\ x \in Number
        /\ y \in Number
        /\ GCD(x, y) = GCD(M, N))'

@!!END

@!!BEGIN
@!!type:obligation
@!!id:15
@!!loc:61:5:61:7
@!!status:proved
@!!prover:zenon
@!!meth:time-limit: 10
@!!already:true
@!!END

@!!BEGIN
@!!type:obligation
@!!id:16
@!!loc:61:8:61:12
@!!status:trivial
@!!prover:tlapm
@!!already:false
@!!END

@!!BEGIN
@!!type:obligation
@!!id:17
@!!loc:61:14:61:18
@!!status:trivial
@!!prover:tlapm
@!!already:false
@!!END

@!!BEGIN
@!!type:obligation
@!!id:18
@!!loc:61:20:61:24
@!!status:trivial
@!!prover:tlapm
@!!already:false
@!!END

@!!BEGIN
@!!type:obligation
@!!id:19
@!!loc:61:26:61:38
@!!status:trivial
@!!prover:tlapm
@!!already:false
@!!END

@!!BEGIN
@!!type:obligation
@!!id:20
@!!loc:57:5:57:7
@!!status:proved
@!!prover:smt
@!!meth:time-limit: 5
@!!already:true
@!!END

@!!BEGIN
@!!type:obligation
@!!id:21
@!!loc:57:8:57:12
@!!status:trivial
@!!prover:tlapm
@!!already:false
@!!END

@!!BEGIN
@!!type:obligation
@!!id:22
@!!loc:59:5:59:7
@!!status:failed
@!!prover:smt
@!!meth:time-limit: 5
@!!reason:false
@!!already:true
@!!obl:ASSUME NEW CONSTANT M,
       NEW CONSTANT N,
       NEW VARIABLE x,
       NEW VARIABLE y,
       /\ x \in Number
       /\ y \in Number
       /\ GCD(x, y) = GCD(M, N) ,
       \/ /\ x < y
          /\ y' = y - x
          /\ x' = x
       \/ /\ y < x
          /\ x' = x - y
          /\ y' = y ,
       y < x ,
       x - y \in Number /\ ~x < y ,
       \A p, q \in Number : p < q => GCD(p, q) = GCD(p, q - p) 
PROVE  GCD(y', x') = GCD(y, x)

@!!END

@!!BEGIN
@!!type:obligation
@!!id:22
@!!loc:59:5:59:7
@!!status:proved
@!!prover:zenon
@!!meth:time-limit: 10
@!!already:true
@!!END

@!!BEGIN
@!!type:obligation
@!!id:23
@!!loc:59:8:59:12
@!!status:trivial
@!!prover:tlapm
@!!already:false
@!!END

@!!BEGIN
@!!type:obligation
@!!id:24
@!!loc:59:14:59:18
@!!status:trivial
@!!prover:tlapm
@!!already:false
@!!END

@!!BEGIN
@!!type:obligation
@!!id:25
@!!loc:59:20:59:32
@!!status:trivial
@!!prover:tlapm
@!!already:false
@!!END

@!!BEGIN
@!!type:obligation
@!!id:26
@!!loc:73:5:73:7
@!!status:failed
@!!prover:ls4
@!!meth:time-limit: 10
@!!reason:false
@!!already:true
@!!obl:ASSUME NEW CONSTANT M,
       NEW CONSTANT N,
       NEW VARIABLE x,
       NEW VARIABLE y,
       Spec => []InductiveInvariant ,
       InductiveInvariant => ResultCorrect 
PROVE  Spec => []ResultCorrect

@!!END

@!!BEGIN
@!!type:obligation
@!!id:27
@!!loc:73:8:73:11
@!!status:trivial
@!!prover:tlapm
@!!already:false
@!!END

@!!BEGIN
@!!type:obligation
@!!id:28
@!!loc:73:13:73:17
@!!status:trivial
@!!prover:tlapm
@!!already:false
@!!END

@!!BEGIN
@!!type:obligation
@!!id:29
@!!loc:73:19:73:23
@!!status:trivial
@!!prover:tlapm
@!!already:false
@!!END

@!!BEGIN
@!!type:obligation
@!!id:30
@!!loc:67:5:67:7
@!!status:proved
@!!prover:smt
@!!meth:time-limit: 5
@!!already:true
@!!END

@!!BEGIN
@!!type:obligation
@!!id:31
@!!loc:69:5:69:7
@!!status:failed
@!!prover:ls4
@!!meth:time-limit: 10
@!!reason:false
@!!already:true
@!!obl:ASSUME NEW CONSTANT M,
       NEW CONSTANT N,
       NEW VARIABLE x,
       NEW VARIABLE y,
       Init => InductiveInvariant ,
       InductiveInvariant /\ Next => InductiveInvariant' ,
       InductiveInvariant /\ UNCHANGED <<x, y>> => InductiveInvariant' 
PROVE  Init /\ [][Next]_<<x, y>> => []InductiveInvariant

@!!END

@!!BEGIN
@!!type:obligation
@!!id:32
@!!loc:69:8:69:11
@!!status:trivial
@!!prover:tlapm
@!!already:false
@!!END

@!!BEGIN
@!!type:obligation
@!!id:33
@!!loc:69:13:69:25
@!!status:trivial
@!!prover:tlapm
@!!already:false
@!!END

@!!BEGIN
@!!type:obligation
@!!id:34
@!!loc:69:27:69:39
@!!status:trivial
@!!prover:tlapm
@!!already:false
@!!END

@!!BEGIN
@!!type:obligation
@!!id:35
@!!loc:69:41:69:45
@!!status:trivial
@!!prover:tlapm
@!!already:false
@!!END

@!!BEGIN
@!!type:obligation
@!!id:36
@!!loc:71:5:71:7
@!!status:proved
@!!prover:smt
@!!meth:time-limit: 5
@!!already:true
@!!END

@!!BEGIN
@!!type:obligation
@!!id:37
@!!loc:71:8:71:20
@!!status:trivial
@!!prover:tlapm
@!!already:false
@!!END

(* created new "euclid.tlaps/euclid.thy" *)
(* fingerprints written in "euclid.tlaps/fingerprints" *)