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:
- the user types,
- for each new value of the password input, the input is displayed in green if the password is strong, and in red otherwise — for the sake of simplicity, a password is considered strong if there are both letters and numbers in the password,
- if the password is not strong, the user click on the
submitbutton is ignored. Otherwise, the password is set to the value of the password input.
Follows some screenshots of the application in different states:
| 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:
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.
- nodes are control states; and
- edges, also called transitions, link an origin control state to a target control state and may contain a triple
event [guard] / actions. Such triple means that when theeventoccurs, if the machine is in the origin control state and theguardis fulfilled, then theactionsare computed. Additionally, the control state for the machine changes to the target control state.
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.