Password meter modeling

In this section, we will model a simple user interface to further illustrate basic state machine concepts like control state, extended state, transitions, guards, action factories, and commands. We will also introduce the graph editor together with the associated Kingly tooling (graph converter and compiler).

Model

The user interface to specify is a password meter. Visually, the user interface consists of a password input field and a submit password button. Its behavior is the following:

Follows some screenshots of the application in different states:

Initial screen Weak password Strong password
initial screen weak password strong password

In other words, we have the following mapping:

Event Reaction
new value of the password input if the new value is strong, display a green indicator
if the new value is not strong, display a red indicator
submit button click if the password input value is not strong, ignore
if the password input value is strong, submit

As we obliquely introduced in the previous section, a state machine is a function that maps events to reactions (commands) and manages two encapsulated pieces of state: control state and extended state. There are a priori infinitely many ways to pick the encapsulated pieces of state. As the reaction to events (submit button clicked and changes of the password input) differ according to the password strength, we will have two control states corresponding to weak passwords and strong passwords.

We add another control state (Idle) that simulates the navigation of the user to the password input page (start event) and that will lead to displaying the initial password meter screen. We also add a terminal control state (Done) in which the machine will not process any event: once a strong password is submitted, there is no further processing to do.

We put any another relevant information in the extended state of the machine. That would be the content of the password input field. Here is what a sample run of the machine would look like:

Control state Extended state Event Commands New control state New extended state
Idle input: "" start display initial password screen Weak input: ""
Weak input: "" typed a display weak password screen Weak input: "a"
Weak input: "a" typed 2 display strong password screen Strong input: "a2"
Strong input: "a2" clicked submit display password submitted screen Done input: "a2"
Weak input: "a" typed b display weak password screen Weak input: "ab"
Weak input: "ab" clicked submit Weak input: "ab"

Take a moment to convince yourself that the machine behavior indeed corresponds to the desired password meter behavior by comparing the event/reaction mapping to the sampled machine run. As before, the machine behavior can be accurately represented with a graph that links together the control states with edges that describe the machine’s computation:

password submit fsm

The graph concepts (nodes, edges) map to state machines concepts as follows:

Kingly’s visual formalism has other features that we do not detail here as they are not necessary to understand the models in this section. For a full description of the syntax for edge labels, see here.

When a machine reacts to an event and updates its internal state, we say that it transitions to that new state. We are going to use the term state a lot across the whole documentation. Unless otherwise specified, from now on, when we will talk about the state of the machine, we will refer to the control state of the machine only. To refer to the actual machine state, we will use internal state (that aggregates both control state and extended state).

Free guarantees

Our state machine concisely represents the fact, or property, that whatever input we receive in the Weak control state, it will only go to the Strong control state if some condition is fulfilled (e.g. the password contains both numbers and letters). Similarly, it will only compute the submit password command if the clicked submit event is received while it is in the Strong state.

The starting state and these two properties can be combined into another fundamental property of the design: the machine will compute the submit password command if and only if the password is strong. In short, we are able to reason formally about the machine and extract properties from its definition — without even testing the machine. This is just one of the many attractive characteristics of state machines which makes them a tool of choice for the robust implementation of applications. In practice, we still have to test. While the machine’s behavior is correct, its constituting functions may be erroneous. We may have inadvertently written wrong the predicate that checks that a password is strong. However, if our guards and action factories are correct, and our visual model is correct, Kingly guarantees that the machine will be correct.

Alright. We modeled the password meter behavior with a state machine that we represented with a graph. Let’s now implement the machine.