If you launch TLC from the Toolbox, it will automagically include a suitable replacement for None in the configuration file that it generates.If you launch TLC from the command line or from the VS Code Extension, you'll have to do it yourself by including something likeNone = Nonein the CONSTANTS section of the configuration file. This mysteriously looking equation instructs TLC to substitute the model value [1] None for the operator None defined in the TLA+ module.The alternative that you indicate of declaring a constant parameter and assumption is also idiomatic. It still makes sense to instantiate that constant by a model value when you run TLC.Stephan[1] See Specifying Systems, section 14.2.1, for more explanations.On 20 Aug 2023, at 01:08, Debersaques Laurent <ldeber...@xxxxxxxxx> wrote:I've been trying to use Leslie's definition for None:None == CHOOSE n : n \notin NatHowever, TLC emits an error when I add this definition to my spec. The error is:TLC attempted to evaluate an unbounded CHOOSE.
Make sure that the _expression_ is of form CHOOSE x \in S: P(x).It seems TLC is unable to pick an arbitrary value if no bound is provided for n. It makes sense, but then I guess one might as well writeCONSTANT None
ASSUME None \notin Natand assign None to an arbitrary string value when checking the model with TLC.On Friday, 5 August 2022 at 16:08:11 UTC+2 Brandon Barker wrote:
Oh, thank you, I'm definitely looking forwad to trying Apalache. (As a personal bonus, I currently develop Scala code, which it is written in).On Tuesday, August 2, 2022 at 1:37:15 PM UTC-4 sh...@informal.systems wrote:Sorry for the late addition here.Apalache has recently added a Variants extension which provides syntactic support for sum types. This extension enables static analysis by Apalache's type checker, which can help catch erroneous use of sum types during specification. Under the hood, our encoding desugars down to something very similar to what Hillel has given.You can use the extension to give a workable representation of a polymorphic option type, useful for representing partial computations. While we haven't developed any battle tested libraries with convenience operators around this extension yet, the following example gives an indication of how those might look:------------------- MODULE OptionExample -----------------------
EXTENDS Naturals, Apalache, Variants
\* @type: UNIT;
UNIT == "U_OF_UNIT"
\* @typeAlias: option = Some(a) | None(UNIT);
\* @type: a => $option;
Some(x) == Variant("Some", x)
\* @type: () => $option;
None == Variant("None", UNIT)
\* @type: $option => Bool;
IsSome(o) == VariantTag(o) = "Some"
\* @type: $option => Bool;
IsNone(o) == VariantTag(o) = "None"
\* @type: $option => a;
GetUnsafe(o) == VariantGetUnsafe("Some", o)
\* @type: (a => b, $option) => $option;
OptionMap(f(_), o) ==
IF IsSome(o)
THEN Some(f(GetUnsafe(o)))
ELSE None
\* @type: Set(a) => $option;
MaxSet(s) ==
LET max(oa, b) ==
IF IsNone(oa)
THEN Some(b)
ELSE IF GetUnsafe(oa) > b THEN oa ELSE Some(b)
IN
ApaFoldSet(max, None, s)
Init == TRUE
Next == TRUE
Inv ==
/\ OptionMap(LAMBDA x: x + 1, Some(2)) = Some(3)
/\ OptionMap(LAMBDA x: x + 1, None) = None
/\ OptionMap(LAMBDA s: s \union {"B"}, Some({"A"})) = Some({"A", "B"})
/\ MaxSet({1,3,4,2}) = Some(4)
/\ MaxSet({}) = None
============================================================You can typecheck this spec in Apalache via `apalache-mc typecheck OptionExample.tla` and confirm that the values computed in the invariant hold with `apalache-mc check --inv=Inv OptionExample.tla`Thanks all, for the replies, they were all helpful in my understanding.Sum types are subtly different from union types. To represent union types in TLC, I usually do something like this:
CONSTANT NotAnInt
ASSUME NotAnInt \notin Int
TypeInv ==
OptionalVal \in Int \union {NotAnInt}To represent optionals as a sum type, I'd instead used a tagged struct:
TypeInv ==
OptionVal \in [type: {"some"}, val: Nat] \union [type: {"none"}]H
On 7/29/2022 7:37 PM, Brandon Barker wrote:Some languages have optional data types (Scala's Option, Java's Optional, Haskell's Maybe, etc), the purpose of which is to obviate the need for null values. As a union type, it can be expressed like:Option a = Some a | None(so an Option of a type a is either a Some of a or it is None.I was trying to think of a good way to do this in an untyped, set-theoretic setting, while trying to avoid accidental equivalence with other values, and came up with something a bit convoluted and arbitrary:None == {{"a", {"fairly unique", {"id:", {"69a86178-6aba-445b-a74b-6769ff09cc29"}}}}}
some(x) == [some: x]
NatOption[x \in Nat] == [some: x] \union {None}This seemed to cause errors in my relatively small, nascent spec once I ran TLC. Unfortunately, I didn't seem to get a line # for the error:The exception was a java.lang.RuntimeException
: Attempted to compare the set {"69a86178-6aba-445b-a74b-6769ff09cc29"} with the value:
"id:"I can try to come up with a a minimal example to reproduce, but maybe it is better to ask how others would model optional values (and types)?--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/c6213ec6-1261-4cc9-b646-9cda6c8d81d3n%40googlegroups.com.--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/57aff553-fb2d-486f-8dc6-54524be0c034n%40googlegroups.com.