CODEWITHSUNDEEP
distributed-computingtla+
Amirhossein Mahdinejad
Amirhossein Mahdinejad

Reputation: 574

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 arguments in programming languages such as python) and use these in another file, call it use.tla, to just use Max and Min without reimplementing them; How is it possible?

Upvotes: 0

Views: 138

Answers (1)

uncleDuo
uncleDuo

Reputation: 31

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

EXTENDS tools

Upvotes: 0

Related Questions