Spec via state machines with enumerated stimuli

state_machine_spec.c

/*
Idea from https://www.youtube.com/watch?v=hkNwku81eh

Aaron Hsu - My favorite verbose programming technique

A very verbose way to produce specifications for a system's state machine.

Sequence-based enumeration can be used as a foundation for defining an executable specification of event-driven behavior.

References:
- https://en.wikipedia.org/wiki/Cleanroom_software_engineering

> The cleanroom process was originally developed by Harlan Mills and several of his colleagues including Alan Hevner at IBM.[1]
> The cleanroom process first saw use in the mid to late 1980s. Demonstration projects within the military began in the early 1990s.[2] Recent work on the cleanroom process has examined fusing cleanroom with the automated verification capabilities provided by specifications expressed in CSP.[3]

*/

#include <assert.h>
#include <stdbool.h>
#include <stdio.h>
#include <string.h>
#include <stdlib.h>

/*

Security Alarm example
----------------------

"Cleanroom people"

An alarm with a trip-wire that triggers the alarm when tripped.

An input device where you can type numbers 0-9 to type a code that will toggle the alarm off

1 The security alarm has a detector that sends a trip signal when motion is detected
2 The security alarm is activted by pressing the Set button
3 The set button is illuminated when the security alarm is set
4 If a trip signal occurs when the security alarm is set, a high pitched tone (Alarm) is heard
5 A three-digit code must be entred to turn off the alarm tone
6 Correct entry of the code deactivates the security alarm
7 If a mistake is made when entering the code, the user must press the Clear button before typing the code

*/

// Abstraction of the stimuli for the alarm
enum Alarm_Stimuli
{
	Alarm_Stimuli_None,
	Alarm_Stimuli_Set, // sets the alarm on
	Alarm_Stimuli_Trip, // the tripwire detected
	Alarm_Stimuli_BadDigit, // type a bad digit
	Alarm_Stimuli_Clear, // reset after typing a bad digit
	Alarm_Stimuli_GoodDigit, // type a good digit
	Num_Alarm_Stimuli,
};

char*
stimuli_desc (enum Alarm_Stimuli stimuli)
{
	switch (stimuli) {
	case Alarm_Stimuli_None:
		return "none";
	case Alarm_Stimuli_Set:
		return "set";
	case Alarm_Stimuli_Trip:
		return "trip";
	case Alarm_Stimuli_BadDigit:
		return "bad";
	case Alarm_Stimuli_Clear:
		return "clear";
	case Alarm_Stimuli_GoodDigit:
		return "good";
	case Num_Alarm_Stimuli:
		return "";
	}
	return "";
}

enum Alarm_Response
{
	Alarm_Response_None,
	Alarm_Response_Alarm_Off,
	Alarm_Response_Alarm_On,
	Alarm_Response_Light_Off,
	Alarm_Response_Light_On,
	Alarm_Response_Invalid,
};

char*
desc (enum Alarm_Response response)
{
	switch (response) {
	case Alarm_Response_None:
		return "No response";
	case Alarm_Response_Alarm_Off:
		return "Alarm Off";
	case Alarm_Response_Alarm_On:
		return "Alarm On";
	case Alarm_Response_Light_Off:
		return "Light Off";
	case Alarm_Response_Light_On:
		return "Light On";
	case Alarm_Response_Invalid:
		assert (false);
		return "Invalid";
	}
	return "";
}

/*

The basic idea is that we represent the state machine as a sequence of states,
and to reduce the explosion of those states, we try to find the canonical
sequence that they can be reduced to.

Another idea is that we convert stimuli into a state sequence by doing:

state sequence + offset produced by stimuli = new state sequence

i.e. if we have a state Initial (_), then receiving stimuli foo finds state _ + offset of foo. So for the stimuli set (offset 1), we find _ + 1, which in the list below would be `S`

To avoid combinatorial explosion, it's maybe best not to specify the whole system in this way.

How to think about the problem:
- responses we care about
- abstract stimuli we care about. For instance good digits vs bad digits instead of 0-9

 */

enum StateSequence
{
	// Important: states must be enumerated in the same order as the stimuli enumeration, for the offsets to allow indexing into the state sequence.

	Initial,
	Listen, // ... suspends to get stimuli ...
	_,
	S,
	T,
	B,
	C,
	G,
	S_,
	S_S,
	S_T,
	S_B,
	S_C,
	S_G,
	S_S_,
	S_T_,
	S_T_S,
	S_T_T,
	S_T_B,
	S_T_C,
	S_T_G,
	S_C_,
	S_C_S,
	S_C_T,
	S_C_B,
	S_C_C,
	S_C_G,
	S_G_,
	S_G_S,
	S_G_T,
	S_G_B,
	S_G_C,
	S_G_G,
	S_B_,
	S_B_S,
	S_B_T,
	S_B_B,
	S_B_C,
	S_B_G,
	S_T_B_,
	S_T_B_S,
	S_T_B_T,
	S_T_B_B,
	S_T_B_C,
	S_T_B_G,
	S_T_C_,
	S_T_C_S,
	S_T_C_T,
	S_T_C_B,
	S_T_C_C,
	S_T_C_G,
	S_T_G_,
	S_T_G_S,
	S_T_G_T,
	S_T_G_B,
	S_T_G_C,
	S_T_G_G,
	S_B_G_,
	S_G_G_,
	S_G_G_S,
	S_G_G_T,
	S_G_G_B,
	S_G_G_C,
	S_G_G_G,
	S_T_G_G_,
	S_T_G_G_S,
	S_T_G_G_T,
	S_T_G_G_B,
	S_T_G_G_C,
	S_T_G_G_G,

	S_End,
};

struct
{
	enum StateSequence self; // for asserting we have specified this case as valid
	enum Alarm_Response response;
	enum Alarm_Response response2;
	enum StateSequence next;
} spec[] = {
	[Initial] = { .self = Initial, .next = _ },
	[Listen] = { .self = Listen },

    // Expecting an interaction from the user
	[_] = { .self = Initial, .next = Listen },
	[S] = { 
        // 2 The security alarm is activated by pressing the Set button
        // 3 The set button is illuminated when the security alarm is set
        .self = S, .response = Alarm_Response_Light_On, .next = S_,
    },
	[T] = { .self = T, .next = Initial }, // state that could be prevented by stimuli generation
	[B] = { .self = B, .next = Initial }, // state that could be prevented by stimuli generation
	[C] = { .self = C, .next = Initial }, // state that could be prevented by stimuli generation
	[G] = { .self = G, .next = Initial }, // state that could be prevented by stimuli generation
	// Once set
	[S_] = { .self = S_, .next = Listen },
	[S_S] = { .self = S_S, .response = Alarm_Response_Light_On, .next = S_ },
	[S_T] = { 
         // 2 The security alarm is activated by pressing the Set button
        .self = S_T, .response = Alarm_Response_Alarm_On, .next = S_T_,
    },
	[S_B] = { .self = S_B, .next = S_B_ },
	[S_C] = { .self = S_C, .next = S_ },
	[S_G] = { .self = S_G, .next = S_G_ },
	//
	[S_T_] = { .self = S_T_, .next = Listen },
	[S_T_S] = { .self = S_T_, .next = S_T_ },
	[S_T_T] = { .self = S_T_T, .next = S_T_ },
	[S_T_B] = { .self = S_T_B, .next = S_T_B_ },
	[S_T_C] = { .self = S_T_C, .next = S_T_ },
	[S_T_G] = { .self = S_T_G, .next = S_T_G_ },
	//
	[S_G_] = { .self = S_G_, .next = Listen },
	[S_G_S] = { .self = S_G_S, .next = S_G_ },
	[S_G_T] = { .self = S_G_T, .response = Alarm_Response_Alarm_On, .next = S_T_B_ },
	[S_G_B] = { .self = S_G_B, .next = S_B_ },
	[S_G_C] = { .self = S_G_C, .next = S_ },
	[S_G_G] = { .self = S_G_G, .next = S_G_G_ },
	//
	[S_B_] = { .self = S_B_, .next = Listen },
	[S_B_S] = { .self = S_B_S, .next = S_B_ },
	[S_B_T] = { .self = S_B_T, .response = Alarm_Response_Alarm_On, .next = S_T_B_ },
	[S_B_B] = { .self = S_B_B, .next = S_B_ },
	[S_B_C] = { .self = S_B_C, .next = S_ },
	[S_B_G] = { .next = S_B_ },
	// Tripped but you typed a bad digit, you must clear to be able to type good digits
	[S_T_B_] = { .self = S_T_B_, .next = Listen },
	[S_T_B_S] = { .self = S_T_B_S, .next = S_T_B_ },
	[S_T_B_T] = { .self = S_T_B_T, .next = S_T_B_ },
	[S_T_B_B] = { .self = S_T_B_B, .next = S_T_B_ },
	[S_T_B_C] = { .self = S_T_B_C, .next = S_T_ },
	[S_T_B_G] = { .response = Alarm_Response_Invalid, },
	//
	[S_T_G_] = { .self = S_T_G_, .next = Listen },
	[S_T_G_S] = { .self = S_T_G_S, .next = S_T_G_ },
	[S_T_G_T] = { .self = S_T_G_T, .next = S_T_G_ },
	[S_T_G_B] = { .self = S_T_G_B, .next = S_T_B_ },
	[S_T_G_C] = { .self = S_T_G_C, .next = S_T_ },
	[S_T_G_G] = { .self = S_T_G_G, .next = S_T_G_G_ },
	//
	[S_G_G_] = { .self = S_G_G_, .next = Listen },
	[S_G_G_S] = { .self = S_G_G_S, .next = S_G_G_ },
	[S_G_G_T] = { .self = S_G_G_T, .next = S_T_ },
	[S_G_G_B] = { .self = S_G_G_B, .next = S_B_ },
	[S_G_G_C] = { .self = S_G_G_C, .next = S_ },
	[S_G_G_G] = { .self = S_G_G_G, .response = Alarm_Response_Light_Off, .next = Initial },
	//
	[S_T_G_G_] = { .self = S_T_G_G_, .next = Listen },
	[S_T_G_G_S] = { .self = S_T_G_G_S, .next = S_T_G_G_ },
	[S_T_G_G_T] = { .self = S_T_G_G_T, .next = S_T_G_G_ },
	[S_T_G_G_B] = { .self = S_T_G_G_B, .next = S_T_B_ },
	[S_T_G_G_C] = { .self = S_T_G_G_C, .next = S_T_ },
	[S_T_G_G_G] = { .self = S_T_G_G_G, .response = Alarm_Response_Alarm_Off, .response2 = Alarm_Response_Light_Off, .next = Initial },

	[S_End] = {},
};

unsigned int
allowed_stimuli (enum StateSequence state)
{
	unsigned int allowed = 1 << Alarm_Stimuli_Set;
	if (S_ <= state && state <= S_End) {
		allowed |= 1 << Alarm_Stimuli_Trip;
		allowed |= 1 << Alarm_Stimuli_BadDigit;
		allowed |= 1 << Alarm_Stimuli_Clear;

		if (state != S_B_ && state != S_T_B_) {
			allowed |= 1 << Alarm_Stimuli_GoodDigit;
		}
	}

	return allowed;
}

enum Alarm_Stimuli
parse_stimuli (char* input)
{
	if (strcmp (input, "set") == 0) {
		return Alarm_Stimuli_Set;
	} else if (strcmp (input, "trip") == 0) {
		return Alarm_Stimuli_Trip;
	} else if (strcmp (input, "bad") == 0) {
		return Alarm_Stimuli_BadDigit;
	} else if (strcmp (input, "clear") == 0) {
		return Alarm_Stimuli_Clear;
	} else if (strcmp (input, "good") == 0) {
		return Alarm_Stimuli_GoodDigit;
	}

	return Alarm_Stimuli_None;
}

/*

Canonical sequences
From that we can have weights / markov chains for state transitions which can help us generate test cases.

*/

// Use the spec to make a cli program where you can type a stimuli and get
// responses.

enum StateSequence
interpret (enum StateSequence s)
{
	if (spec[s].self != s) {
		printf ("Invalid state sequence reached: %d\n", s);
		assert (false); // an invalid state sequence was reached
		return s;
	}

	if (spec[s].response) {
		printf ("response: %s\n", desc (spec[s].response));
	}
	if (spec[s].response2) {
		printf ("response: %s\n", desc (spec[s].response2));
	}

	if (spec[s].next == Listen) {
		return s;
	}

	return spec[s].next;
}

int
listen (enum StateSequence state)
{
	char CLI[1024];

	int offset;

	for (;;) {
		printf ("$ ");
		fflush (stdout);
		char* res = fgets (CLI, (int)sizeof CLI, stdin);
		if (!res) {
			printf ("ERROR\n");
			return 0;
		}

		for (char* p = res; *p; p++) {
			if (*p == '\n') {
				*p = '\0';
				break;
			}
		}

		if (strcmp ("quit", res) == 0) {
			exit (0);
		}

		// compute state offset for stimuli
		enum Alarm_Stimuli stimuli = parse_stimuli (res);
		if (stimuli == Alarm_Stimuli_None) {
			printf ("Unrecognized, should be one of {set, good, bad, trip, clear, quit}\n");
			continue;
		}
		unsigned int allowed = allowed_stimuli (state);
		if ((allowed & (1 << stimuli)) == 0) {
			printf ("This stimuli is disallowed considering the current state: %d, allowed: ", state);
			for (int i = 1, n = Num_Alarm_Stimuli; i < n; i++) {
				if (allowed & (1 << i)) {
					printf ("%s%s", i > 1 ? ", " : "", stimuli_desc (i));
				}
			}
			printf ("\n");

			continue;
		}

		offset = stimuli;
		break;
	}
	return offset;
}

int
main (int argc, char** argv)
{
	if (argc > 1) {
		printf ("Usage: %s\n", argv[0]);
		return 0;
	}

	enum StateSequence s = Initial;
	for (;;) {
		s = interpret (s);
		if (spec[s].next == Listen) {
			s += listen (s);
		}
	}

	return 0;
}