<jupyter_start><jupyter_text>Constant expressionsBare statement in a cell is treated as a constant expression and will be immediately evaluated upon cell execution. For example, to a get set of all odd squares of the first ten numbers we may execute:<jupyter_code>{sq \in {x*x: x \in 1..10}: sq%2=1}<jupyter_output><empty_output><jupyter_text>For more complex expression it is handy to use `LET ... IN ...` construct:<jupyter_code>LET
    n_nodes == 3
    nodes == 1..n_nodes
    quorum(mask) == Cardinality({i \in DOMAIN mask: mask[i] = 1}) >= (n_nodes \div 2 + 1)
    new_status(old_status, vmask, emask) ==
        CASE ~ quorum(vmask) -> "disabled"
        [] old_status = "disabled" -> "recovery"
        [] (old_status = "recovered" /\ vmask = emask) -> "online"
        [] OTHER -> old_status
IN
    new_status("recovered", <<1, 1, 0>>, <<1, 1, 0>>)<jupyter_output><empty_output><jupyter_text>ModulesCells starting with four dashes are treated as a module definition. Upon evaluation kernel will perform basic syntax checks with `tla2sany` and report errors if there will be any. Let's evaluate `DieHard` spec from [The TLA+ Video Course](https://lamport.azurewebsites.net/video/videos.html):<jupyter_code>--------------------------- MODULE DieHard ----------------------------
EXTENDS Naturals
VARIABLES big,   \* The number of gallons of water in the 5 gallon jug.
          small  \* The number of gallons of water in the 3 gallon jug.

Min(m,n) == IF m < n THEN m ELSE n
TypeOK   == small \in 0..3 /\ big   \in 0..5

Init          == big    = 0 /\ small  = 0
FillSmallJug  == small' = 3 /\ big'   = big
FillBigJug    == big'   = 5 /\ small' = small
EmptySmallJug == small' = 0 /\ big'   = big
EmptyBigJug   == big'   = 0 /\ small' = small

SmallToBig    == /\ big'   = Min(big + small, 5)
                 /\ small' = small - (big' - big)

BigToSmall    == /\ small' = Min(big + small, 3) 
                 /\ big'   = big - (small' - small)

Next ==  \/ FillSmallJug 
         \/ FillBigJug    
         \/ EmptySmallJug 
         \/ EmptyBigJug    
         \/ SmallToBig    
         \/ BigToSmall    

Spec == Init /\ [][Next]_<<big, small>>
NotSolved == big # 4

=============================================================================<jupyter_output><empty_output><jupyter_text>TLCTo check a model `TLC` will need a configuration file. In that file among a lot of things we may:* Set model constants to specific values* Provide the name of specification formula or Init/Next formulas* Mention symmetriesTo indicate kernel that given cell is a `TLC` config cell needs to be started with line `%tlc:ModelName` where ModelName is the name of a module to be checked. The module should be already evaluated in some other cell before running `TLC`. Upon evaluation of such a cell kernel will run `TLC` with the number of workers equal to number of cores on the jupyter server. Any `TLC` output will be dynamically sent to the notebook. By default `TLC` prints it's progress once in a minute.For example, to check `DieHard` model we may run:<jupyter_code>%tlc:DieHard
SPECIFICATION Spec
INVARIANTS TypeOK NotSolved<jupyter_output><empty_output><jupyter_text>If we need to pass some custom command-line option to `TLC` we may put them after the `%tlc:ModelName` prefix. Like that:<jupyter_code>%tlc:DieHard -deadlock -workers 1
SPECIFICATION Spec
INVARIANTS TypeOK<jupyter_output><empty_output>
{'fraction_non_alphanumeric': 0.14055164319248825, 'fraction_numerical': 0.009683098591549295, 'mean_word_length': 3.1321212121212123, 'pattern_counts': {'":': 0, '<': 28, '<?xml version=': 0, '>': 32, 'https://': 1, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'chain_length': '5', 'dir': 'jupyter-structured-clean-dedup', 'id': '535109', 'license': 'BSD-3-Clause', 'n_tokens_mistral': 1101, 'n_tokens_neox': 1026, 'n_words': 394, 'path': 'examples/intro.ipynb', 'repo_name': 'Alexander-N/tlaplus_jupyter', 'size': '3408'}