DOMAIN error when running final spec in Behaviors page

[danielmai]

When I try to execute the spec at the bottom of the Behaviors page, I get an error. Here's the spec:

---- MODULE flags ----
EXTENDS TLC, Integers
(* --algorithm flags
variables flags = [1..3 -> BOOLEAN], next = TRUE;
begin
  while next do
    with f \in DOMAIN flags, n \in BOOLEAN do
      flags[f] := ~flags[f];
      next := n;
    end with;
  end while;
end algorithm; *)

====

and here's the error I got after running the model checker:

TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.RuntimeException
: Attempted to apply the operator DOMAIN to a non-function
(a set of the form [S -> T])

When I evaluate [1..3 -> BOOLEAN], its value is

{ <<FALSE, FALSE, FALSE>>,
     <<FALSE, FALSE, TRUE>>,
     <<FALSE, TRUE, FALSE>>,
     <<FALSE, TRUE, TRUE>>,
     <<TRUE, FALSE, FALSE>>,
     <<TRUE, FALSE, TRUE>>,
     <<TRUE, TRUE, FALSE>>,
     <<TRUE, TRUE, TRUE>> }

So I see that flags a set, not a function, which explains the error "Attempted to apply the operator DOMAIN to a non-function". I'm not sure what's the proper way to make flags a function for the three boolean flags.

[hwayne]

Yeah my mistake, it's supposed to be flags \in, not flag =. I'll push the change as soon as I'm off the train.

On Wed, May 17, 2017, 12:11 AM Daniel Mai notifications@github.com wrote:

When I try to execute the spec at the bottom of the Behaviors https://learntla.com/pluscal/behaviors/ page, I get an error. Here's the spec:

---- MODULE flags ---- EXTENDS TLC, Integers ( --algorithm flags variables flags = [1..3 -> BOOLEAN], next = TRUE; begin while next do with f \in DOMAIN flags, n \in BOOLEAN do flags[f] := ~flags[f]; next := n; end with; end while; end algorithm; )

====

and here's the error I got after running the model checker:

TLC threw an unexpected exception. This was probably caused by an error in the spec or model. See the User Output or TLC Console for clues to what happened. The exception was a java.lang.RuntimeException : Attempted to apply the operator DOMAIN to a non-function (a set of the form [S -> T])

When I evaluate [1..3 -> BOOLEAN], its value is

{ <<FALSE, FALSE, FALSE>>, <<FALSE, FALSE, TRUE>>, <<FALSE, TRUE, FALSE>>, <<FALSE, TRUE, TRUE>>, <<TRUE, FALSE, FALSE>>, <<TRUE, FALSE, TRUE>>, <<TRUE, TRUE, FALSE>>, <<TRUE, TRUE, TRUE>> }

So I see that flags a set, not a function, which explains the error "Attempted to apply the operator DOMAIN to a non-function". I'm not sure what's the proper way to make flags a function for the three boolean flags.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/hwayne/learntla/issues/3, or mute the thread https://github.com/notifications/unsubscribe-auth/ACiXdHHOnHAb4m_ZshvvalBoR1LAbSeHks5r6oFugaJpZM4NdYeV .

[hwayne]

Fixed in https://github.com/hwayne/learntla/commit/ef57679280ca8e50fa126eb38411bfcd256500e1!