python (65.1k questions)

javascript (44.2k questions)

reactjs (22.7k questions)

java (20.8k questions)

c# (17.4k questions)

html (16.3k questions)

r (13.7k questions)

android (12.9k questions)

Questions - tla+

What temporal formula to use for knapsack problem?

In "Practical TLA+" by Hillel Wayne, Chapter 3 goes over an implementation of the Knapsack Problem in PlusCal. Although I understand the implementation, I don't understand how to run it. He ...
test-img

Seanny123

visual-studio-code

knapsack-problem

tla+

pluscal

Votes: 0

Answers: 2

Latest Answer

It's under "model overview > what is the behavior spec".
test-img

Hovercouch

Import operators from TLA+ module into another file

Suppose that we have these operators in tools.tla file: ---- MODULE PT ---- Max(x, y) == IF x > y THEN x ELSE y Min(x, y) == IF x < y THEN x ELSE y ===== and we want to pass values (like argum...
test-img

Amirhossein Mahdinejad

distributed-computing

tla+

Votes: 0

Answers: 1

Latest Answer

I meet the similar problem and that's my solutions: File -> Open module -> Add TLA+ module -> tools.tla The empty tools.tla will be created, write your codes. Go back to another file and E...
test-img

uncleDuo

How to use git effectively with TLA+ toolbox

The TLA+ toolbox creates a lot of files and directories. What's a good way to work with the spec and the model and keep them versioned in git, and also use the toolbox? What does a normal workflow loo...
test-img

Jeff

tla+

Votes: 0

Answers: 2

Latest Answer

I have completely ignored *.toolbox in my .gitignore. This means model configuration is not preserved in the repo which is not ideal. A good workflow is possible with the VS Code plugin that relies on...
test-img

felipecrv

Posts

Questions

Blogs

Jobs