Data Structures

items = []
items.append(1)
items.insert(0, 2)
items.remove(1)
item = items.pop()

s = set()
s.add(1)
s.discard(2)
union = s1.union(s2)
intersection = s1.intersection(s2)

d = {}
d["key"] = "value"
value = d.get("key", default)
keys = d.keys()
values = d.values()

# Generic set (allows dicts, lists as elements)
gs = genericset()
gs.add([1, 2, 3])
gs.add({"key": "value"})  # Dicts allowed

# Generic map (allows dicts, lists as keys)
gm = genericmap()
gm[[1, 2]] = "value"
gm[{"id": 1}] = "data"    # Dict keys allowed

# ❌ WRONG: Generic collections in global state
action Init:
    global_set = genericset()  # Bad - state hashing issue

# ✅ CORRECT: Generic collections in local scope
atomic action Process:
    local_set = genericset()   # OK - local variable
    local_set.add([1, 2])
    process(local_set)

b = bag()
b.add(1)
b.add(1)  # Can add duplicates
count = b.count(1)  # Returns 2

State = enum('INIT', 'RUNNING', 'DONE')
current = State.INIT

# Iterate over enum values
for state in dir(State):
    # Process each state

msg = record(id=1, payload="data")
msg.id = 2  # Mutable

config = struct(timeout=30, retries=3)
# config.timeout = 60  # ERROR: immutable

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31

# Example 0029: Lists
# Ordered collection of elements
# Demonstrates: list operations (append, insert, pop, remove)

MAX = 3

action Init:
    items = []

atomic action AddItem:
    require len(items) < MAX

    # Common list operations
    items.append(len(items))  # Add to end

    if len(items) == 2:
        items.insert(0, -1)  # Insert at position

atomic action RemoveItem:
    require len(items) > 0

    # Remove operations
    if len(items) > 0:
        items.pop()  # Remove from end

# Lists maintain insertion order
# items progression: [] -> [0] -> [0,1] -> [-1,0,1] -> [-1,0] -> [-1] -> []

atomic action NoOp:
    if len(items) == 0 or len(items) >= MAX:
        pass

StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2}
Nodes: 9, queued: 0
Valid Nodes: 9 Unique states: 9
IsLive: true
PASSED: Model checker completed successfully

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29

# Example 0030: Sets
# Unordered collection of unique elements
# Demonstrates: set operations (add, remove, discard, union, intersection)

action Init:
    set_a = set([1, 2])
    set_b = set([2, 3])
    result = set()

atomic action SetOperations:
    require len(result) == 0

    # Set operations
    set_a.add(4)         # Add element
    set_b.discard(2)     # Remove if exists (no error if missing)

    # Set algebra
    result = set_a.union(set_b)        # {1, 2, 3, 4}
    # result = set_a.intersection(set_b)  # Common elements
    # result = set_a.difference(set_b)     # In A but not B

# Sets automatically handle uniqueness
# set_a: {1, 2} -> {1, 2, 4}
# set_b: {2, 3} -> {3}
# result: {1, 2, 3, 4}

atomic action NoOp:
    if len(result) > 0:
        pass

StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2}
Nodes: 2, queued: 0
Valid Nodes: 2 Unique states: 2
IsLive: true
PASSED: Model checker completed successfully

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35

# Example 0031: Dictionaries
# Key-value pairs (keys must be hashable)
# Demonstrates: dict operations (get, set, pop, keys, values)

action Init:
    counts = {}
    total = 0

atomic action UpdateCounts:
    require total < 3

    key = "count_" + str(total)

    # Dictionary operations
    counts[key] = total        # Set value

    # Safe access
    value = counts.get(key, 0) # Get with default
    total = total + value + 1

atomic action CheckKeys:
    require len(counts) > 0

    # Iterate over keys
    for k in counts.keys():
        # Access values
        v = counts[k]
        break

# Dictionaries maintain key uniqueness
# counts: {} -> {"count_0": 0} -> {"count_0": 0, "count_1": 1} -> ...

atomic action NoOp:
    if total >= 3:
        pass

StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2}
Nodes: 3, queued: 0
Valid Nodes: 3 Unique states: 3
IsLive: true
PASSED: Model checker completed successfully

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30

# Example 0032: Generic Set
# Set that supports non-hashable elements (e.g., dicts, lists)
# Demonstrates: genericset for complex types

action Init:
    items = genericset()
    count = 0

atomic action AddComplexItem:
    require count < 2

    # Can add non-hashable types like dicts
    item = {"id": count, "status": "pending"}
    items.add(item)
    count = count + 1

atomic action UpdateItem:
    require len(items) > 0

    # Add duplicate - will not increase size
    duplicate = {"id": 0, "status": "pending"}
    items.add(duplicate)

# genericset handles non-hashable elements
# Regular set would fail with dict keys
# items: {} -> {{"id":0, "status":"pending"}} -> adds {"id":1,...}

atomic action NoOp:
    if count >= 2:
        pass

StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2}
Nodes: 3, queued: 0
Valid Nodes: 3 Unique states: 3
IsLive: true
PASSED: Model checker completed successfully

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39

# Example 0033: Generic Map
# Map that supports non-hashable keys
# Demonstrates: genericmap for complex key types
# NOTE: genericmap currently has limitations with state persistence
#       This example shows the API but uses regular dict for state

action Init:
    result = ""
    count = 0

atomic func UseGenericMap():
    # genericmap can be used in local scope
    lookup = genericmap()

    # Use list as key (not possible with regular dict)
    key1 = [1, "a"]
    key2 = [2, "b"]

    lookup[key1] = "value1"
    lookup[key2] = "value2"

    # Retrieve values
    if key1 in lookup:
        return lookup[key1]
    return "none"

atomic action TestGenericMap:
    require count < 2

    count = count + 1
    result = UseGenericMap()

# genericmap allows non-hashable keys like lists/dicts
# But may have limitations when part of persistent state
# Use for local computations within atomic blocks

atomic action NoOp:
    if count >= 2:
        pass

StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2}
Nodes: 3, queued: 0
Valid Nodes: 3 Unique states: 3
IsLive: true
PASSED: Model checker completed successfully

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30

# Example 0034: Bags (Multisets)
# Collection where duplicates are allowed and counted
# Demonstrates: bag operations (add, remove, count)

action Init:
    items = bag()
    total = 0

atomic action AddItems:
    require total < 4

    # Bags allow duplicates
    items.add(1)
    items.add(2)
    items.add(1)  # Duplicate allowed
    total = total + 1

atomic action RemoveItem:
    require len(items) > 0

    # Remove one instance
    items.discard(1)

# Bags are like multisets - order doesn't matter but count does
# bag([1, 2, 1]) == bag([1, 1, 2]) == bag([2, 1, 1])
# but bag([1, 1, 2]) != bag([1, 2])

atomic action NoOp:
    if total >= 4:
        pass

StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2}
Nodes: 25, queued: 0
Valid Nodes: 25 Unique states: 25
IsLive: true
PASSED: Model checker completed successfully

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34

# Example 0035: Enums
# Named constants for better readability
# Demonstrates: enum definition and usage

# Define enum at top level
State = enum('INIT', 'RUNNING', 'DONE')

action Init:
    current_state = State.INIT

atomic action Transition:
    require current_state != State.DONE

    # State machine using enum
    if current_state == State.INIT:
        current_state = State.RUNNING
    elif current_state == State.RUNNING:
        current_state = State.DONE

# Enums are syntactic sugar over strings
# State.INIT == 'INIT' is true

# Can iterate over enum values
atomic action CheckAllStates:
    require current_state == State.DONE

    # dir() returns all enum values
    for state in dir(State):
        # Process each state value
        pass

atomic action NoOp:
    if current_state == State.DONE:
        pass

StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2}
Nodes: 3, queued: 0
Valid Nodes: 3 Unique states: 3
IsLive: true
PASSED: Model checker completed successfully

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28

# Example 0036: Records
# Mutable named structures
# Demonstrates: record creation and field access

action Init:
    # Create record with named fields
    user = record(name="alice", age=25, active=True)
    counter = 0

atomic action UpdateRecord:
    require counter < 2

    counter = counter + 1

    # Access and modify fields
    user.age = user.age + 1

    if counter == 2:
        user.active = False

# Records are mutable structures
# user: {name:"alice", age:25, active:True}
#    -> {name:"alice", age:26, active:True}
#    -> {name:"alice", age:27, active:False}

atomic action NoOp:
    if counter >= 2:
        pass

StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2}
Nodes: 3, queued: 0
Valid Nodes: 3 Unique states: 3
IsLive: true
PASSED: Model checker completed successfully

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28

# Example 0037: Structs
# Immutable named structures (from Starlark)
# Demonstrates: struct creation and immutability

# Define struct at top level
Config = struct(max_retries=3, timeout=30, debug=False)

action Init:
    # Structs are immutable
    config = Config
    attempts = 0

atomic action UseConfig:
    require attempts < config.max_retries

    # Can read fields
    max_val = config.max_retries
    attempts = attempts + 1

# Attempting to modify would error:
# config.max_retries = 5  # ERROR: cannot assign to struct field

# Structs are useful for constants that shouldn't change
# Unlike records, they are immutable

atomic action NoOp:
    if attempts >= config.max_retries:
        pass

StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2}
Nodes: 4, queued: 0
Valid Nodes: 4 Unique states: 4
IsLive: true
PASSED: Model checker completed successfully

gdoc_arrow_left_alt Assertions Control Flow gdoc_arrow_right_alt