tla+

How to declare functions that is neither entire nor surjective in TLA+

I've been stuck on how what is the best way to define a relation between 2 sets, that do not comprise a function (not entire). As I come from Alloy, relations are very intuitive for me, where in TLA+ this is a problem for me.

Let's say I have these 2 sets:

Set1 == {"A","B","C"}
Set2 == {1,2,3}

How do I define function SS with A mapped to 1 and B mapped to 3, and nothing more.

I know functions are entire, thus we should have something like this, SS == [s \in Set1 |-> CASE ...]

However, I don't want the function to be entire. Also, I usually misunderstand functions with records, that have 1 key only.

But is there any other way to do this?

Solution

  • Option 1: define a set of tuple-pairs with some helper functions.

    Option 2: extend the TLC module and use the operators it defines:

    map == “A” :> 1 @@ “B” :> 3

    Option 3: use record syntax since your domain is a set of strings:

    map == [A |-> 1, B |-> 3]

    Option 4: only define your map for a subset of your domain:

    map == [x \in Set1 \ {“C”} |-> …]