I realized my mistake!
I put the property we are trying to verify as the temporal formula. Spec is the temporal formula, and LM_Inner_ISpec is a property.
The model checker now runs and finds no errors.
Nicolas
On Tuesday, July 2, 2019 at 11:32:15 AM UTC-4, Nicolas Duchêne wrote:
Hi all,
I'm just starting off in using TLA+ and TLC, and have been trying to check the TLC-adapted MCWriteThroughCache specification.
The declared constants I chose are:
-------------------------
Val <- [model value]{v1,v2}
Proc <- [model value]{p1,p2}
QLen <- 1
InitMemInt <- MCInitMenInt
Adr <- [model value]{a1}
Send(p, d, oldMemInt, newMemInt) <- MCSend(p,d,oldMemInt,newMemInt)
Reply(p,d,oldMemInt,newMemInt) <- MCReply(p,d,oldMemInt,newMemInt)
-------------------------
These are the values I found in the cfg file that is provided with the specification, and so I simply input them in the model overview section because I was having some trouble using the command line version of TLC.
The part I'm not sure about is the Send(...)<-MCSend(...)
declaration (along with the reply analogue).
Does it correctly reproduce the Send <- MCSend declaration in the provided cfg file?
How do I provide the "InitMemInt <- MCInitMemInt" declaration to TLC with the toolbox GUI? Is my use of Ordinary assignment correct?
I use the LM_Inner_ISpec temporal formula and the LM_Inner_TypeInvariant invariant.
When I run the model checker with these declarations, I get a java.lang.NullPointerException error.
The TLC Errors output shows:
"
>The subscript of the next-state relation specified by the specification
does not seem to contain the state variable ctl
The subscript of the next-state relation specified by the specification
does not seem to contain the state variable wmem
The subscript of the next-state relation specified by the specification
does not seem to contain the state variable memQ
The subscript of the next-state relation specified by the specification
does not seem to contain the state variable cache
In evaluation, the identifier memQ is either undefined or not an operator.
line 117, col 24 to line 117, col 27 of module WriteThroughCacheInstanced
The error occurred when TLC was evaluating the nested
expressions at the following positions:
0. Line 51, column 19 to line 54, column 42 in MCWriteThroughCache
1. Line 51, column 22 to line 51, column 40 in MCWriteThroughCache
2. Line 51, column 22 to line 51, column 25 in MCWriteThroughCache
3. Line 32, column 12 to line 32, column 15 in MCWriteThroughCache
4. Line 117, column 3 to line 123, column 17 in WriteThroughCacheInstanced
5. Line 123, column 6 to line 123, column 17 in WriteThroughCacheInstanced
6. Line 123, column 6 to line 123, column 6 in WriteThroughCacheInstanced
7. Line 117, column 7 to line 122, column 61 in WriteThroughCacheInstanced
8. Line 117, column 15 to line 117, column 28 in WriteThroughCacheInstanced
9. Line 117, column 20 to line 117, column 28 in WriteThroughCacheInstanced
10. Line 117, column 24 to line 117, column 27 in WriteThroughCacheInstanced
"
I would appreciate any pointers!
Thanks,
Nicolas Duchêne