Stack Overflow
Stack Overflow

Questions tagged [tlc]

TLC is a model checker for specifications written in TLA+. The source code of TLC can be found in this GitHub repository.

17 questions
13
votes
1 answer

TLA+ How to visualize the state graph

I a new TLA+ user. I read that the TLA toolbox allows us to visualize the state graph after completion of model-checking. In order to do so dot needs to be installed which I did. But I didn't figure out how to launch the visualization. Can I do it…
Bad Retsuko
  • 133
  • 6
3
votes
1 answer

\in works, while \subseteq gives a "identifier undefined" error

I have the following spec: ------------------------------ MODULE Group ------------------------------ CONSTANTS People VARIABLES members Init == members \subseteq People Next == members' = members Group == Init /\…
Philip
  • 1,532
  • 12
  • 23
2
votes
1 answer

TLA+ error : The invariant Invariants is not a state predicate

In my spec, I'm trying to check if a change in a sequence is either -1, 0 or 1. I described this invariant as below : PVariance == Len(waitingRoomP') - Len(waitingRoomP) \in {-1,0,1} CVariance == Len(waitingRoomC') - Len(waitingRoomC) \in…
devio
  • 1,147
  • 5
  • 15
  • 41
2
votes
1 answer

TLA+ toolbox error running model: overridden value Nat

I've been hitting the following error in TLA+ toolbox for a few days now in various contexts: "Attempted to compute the number of elements in the overridden value Nat.". The following is the simplest module that I've come up with that will…
Noah Watkins
  • 5,446
  • 3
  • 34
  • 47
1
vote
1 answer

How to make TLC add label information for action name in its producted dot file?

When using TLA+ and TLC, if I want to generate a visualizable state graph, I can check the checkbox of "TLC options"->"feature"->"Visualize state graph after completion of model checking". This can generate a pdf file of the state graph as well as a…
fwhdzh
  • 21
  • 3
1
vote
1 answer

Show trace name on nth-level

Question When using CLI, how to have it show n-th level action trace name (and symbolic arguments names) when an error occurs? Command: java -jar tla2tools.jar Test.tla Normal For example, with: Spec == Init /\ [][Next]_<> it…
jmpsabisb
  • 182
  • 1
  • 10
1
vote
0 answers

How to correctly use module instantiation in TLA+ and TLC

I want to instantiate a module multiple times in a TLA specification, e.g., in a communication network consisting of multiple but identical nodes, executing the same protocol. My problem is that I haven't found a way to do this without having to…
naumb
  • 11
  • 3
1
vote
1 answer

S-Function uint64_T input/output for simulink code generation error

I am attempting to generate C code with simulink coder for a model with an S-Function on Matlab 2020b. The S-Function contains an int64 input and an int64 output. The update diagram and simulink simulation work fine, therefore my s-function is…
hockey_buzz
  • 39
  • 3
1
vote
3 answers

How can I assign sequences to constants in the CONSTANTS section of a TLA+ configuration file?

I've tried CONSTANTS seq = <<5,6,7>> but TLC gives me a syntax error: Error: TLC found an error in the configuration file at line 1. It was expecting = or <- and didn't find it. I've also tried to include the Sequences module in the…
luvieere
  • 37,065
  • 18
  • 127
  • 179
0
votes
1 answer

Telethon SendReactionRequest: a TLObject was expected but found something else

This represent the Telethon request to send the reaction on the post of the public channel.when run the code I got some error when the code try to run this "SendReactionRequest" they catch the error of TLC object import asyncio from telethon.sync…
Muhammad HAMMAD ASGHAR
  • 1
  • 1
0
votes
1 answer

How do I override only the "top-level" operator in TLC?

I have two specs like this: ---- MODULE Spec ---- VARIABLE x Init == x \in BOOLEAN Next == x' = ~x Spec == Init /\ [][Next]_x ==== ---- MODULE MCSpec ---- EXTENDS Spec MCInit == Init /\ x = FALSE \* Optimization MCSpec == MCInit /\…
Hovercouch
  • 1,962
  • 12
  • 12
0
votes
1 answer

Why is TLC reporting errors on valid states?

I have the following specification for a queue: ------------------------------- MODULE queue ------------------------------- EXTENDS Naturals CONSTANT L (* The fixed max length of the queue *) VARIABLE q (* Represents the queue as the number of…
Andry
  • 16,172
  • 27
  • 138
  • 246
0
votes
1 answer

How to abort a macports portfile on an error condition?

I working on a version bump on the cc65 and encountered a problem with the linuxdoc-tools. Since I can't fix the linuxdoc-tools and there is a simple workaround possible I decided to add an if statement to inform the user together with the…
Martin
  • 11,577
  • 16
  • 80
  • 110
0
votes
1 answer

How do I use a self-signed certificate to sniff encrypted traffic from client to some website?

For my Internet Security course, I was given a project where I am to ultimately take advantage of the "remember my password" on a site by creating a certificate, manually put it in my "clients" browser to be trusted and then be able to sniff all…
helplessKid
  • 15
  • 3
0
votes
1 answer

Is it possible to use tlc while do stateflow design in MATLAB Simulink?

The tlc can be saved as text file and has tracebilty. Is it possible to using tlc in stateflow design? Or Any other suggestion to keep the tracebilty feature in sateflow project?
Redefl
  • 125
  • 6
1
2