Solving with TLA in Star Wars KOTOR 2

Posted on October 08, 2022

TLDR

These are just my notes on an exercise in TLA+. I think it's a good excuse to play with sequence manipulation in TLA+ on an entirely impractical application. In this case, to solve a puzzle from a Star Wars game. Someday, I will write a story about a Jedi learning TLA+.

Wait, whats TLA+? Whats this for?

TLA+ is a modeling language. You can use it to write specifications. In TLA+, a specification is a set of formulas that could be true or false. Then you pass the specification to a model checker, which tries lots of things and tells you when and how your invariants or liveness properties fail.

It's been successfully applied to distributed systems and protocols to identify when they break. I recommend the TLA+ Video Course to learn more. Or Hillel Wayne's writing. Or Pron's writing.

Problem

In Star Wars: Knights of the Old Republic II you encounter a computer that must be repaired. After putting in a great deal of work, you encounter one final problem. There is one equation whose operators are missing: 6_2_9_8_1=13. Can you write a specification in TLA+ to identify the operators that satisfy it?

Approach 1: Predetermined Operators and Brute Force

This is essentially brute force.

1. Choose a set of operators.
2. Upon evaluation, does it equal 13? If so, you're done.

--------------------------------- MODULE dxun ----------------------------------
EXTENDS Integers, Sequences
VARIABLES pass, position, operator_decisions, operands, operand_position
vars == <<pass, position, operator_decisions, operands, operand_position>>

Operator == {"*", "/", "+", "-"}

PassTypeOK == pass \in 1..2
PositionTypeOK == position \in Nat
OperandPositionTypeOK == operand_position \in Nat
OperandTypeOK == \A i \in DOMAIN operands: operands[i] \in Int
OperatorDecisionsTypeOK == \A i \in DOMAIN operator_decisions: 
                                operator_decisions[i] \in Operator 
TypeOK == /\ PassTypeOK
          /\ PositionTypeOK
          /\ OperandPositionTypeOK
          /\ OperandTypeOK
          /\ OperatorDecisionsTypeOK

PrecedenceMap(operator) == 
    CASE operator = "*" -> 1
      [] operator = "/" -> 1
      [] operator = "+" -> 2
      [] operator = "-" -> 2

PerformOperation(operation, lhs, rhs) ==
    CASE operation = "*" -> lhs * rhs
      [] operation = "+" -> lhs + rhs
      [] operation = "-" -> lhs - rhs
      [] operation = "/" -> lhs \div rhs

Reduce(operation, seq, index) == 
    LET i == index
        j == index + 1
        lhs == seq[i]
        rhs == seq[j]
        val == PerformOperation(operation, lhs, rhs)
    IN
        SubSeq(operands, 1, i - 1) \o <<val>> 
        \o SubSeq(operands, j+1, Len(operands))

Init == /\ pass = 1
        /\ position = 1
        /\ operands = <<6, 2, 8, 9, 1>>
        /\ operator_decisions \in [1..Len(operands)-1 -> Operator]
        /\ operand_position = 1

AdvanceOperatorPos == 
    LET op == operator_decisions[position] IN
        IF PrecedenceMap(op) > pass
            THEN 
                /\ operand_position' = operand_position + 1
            ELSE 
                UNCHANGED operand_position

Evaluate(index) == 
    LET op == operator_decisions[position] IN
        IF PrecedenceMap(op) = pass
            THEN 
                /\ operands' = Reduce(op, operands, operand_position) 
                /\ UNCHANGED <<operand_position, operator_decisions>>
            ELSE 
                /\ AdvanceOperatorPos
                /\ UNCHANGED <<operator_decisions, operands>>

HandleFirstPass == /\ pass = 1
                   /\ position \in 1..(Len(operator_decisions))
                   /\ Evaluate(position)
                   /\ position' = position + 1
                   /\ UNCHANGED <<pass>>
                          
TransitionToSecondPass == /\ pass = 1
                          /\ position = Len(operator_decisions)+1
                          /\ pass' = 2
                          /\ position' = 1
                          /\ operand_position' = 1
                          /\ UNCHANGED <<operator_decisions, operands>>

HandleSecondPass == /\ pass = 2
                    /\ position \in 1..(Len(operator_decisions))
                    /\ Evaluate(position)
                    /\ position' = position + 1
                    /\ UNCHANGED <<pass>>

Next == \/ HandleFirstPass
        \/ TransitionToSecondPass
        \/ HandleSecondPass 

Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

AlwaysCompletes == <>[](Len(operands) = 1)

NeverEquals13 == Len(operands) = 1 => operands[1] # 13
================================================================================

And, the accompanying configuration.

SPECIFICATION
    Spec

INVARIANTS
    NeverEquals13
    TypeOK

CHECK_DEADLOCK
    FALSE

PROPERTIES
    AlwaysCompletes

Notes

AlwaysCompletes verifies that all evaluations eventually end with exactly one value.

NeverEquals13 is an invariant that fails when the expression evaluates to 13, giving us a satisfying set of operators.

Questions

1. What happens when there is a division by zero?
2. Why is WF_vars necessary to ensure the AlwaysCompletes property?
3. What is the depth of the complete state graph seach?
4. What is the outdegree of the complete state graph?
5. Is there a simpler way to express the reduction operation? That is, do the arithmetic?