model-lang/docs/overview.md

What is model-lang?

The model-lang suite contains the following components:

1. language - the format used to describe behaviors and interactions, built for simplicity, and inspired by the MP language by Mikhail Auguston at NPS
2. parser - reads the modeling language text, checks for proper syntax, and converts it into output for the other tools
3. generator - simulates a model to produce all possible scenarios (within a small scope) as a set of event traces (to check for undesirable scenarios)
4. ... more tools coming soon ...

Language

A model-lang model defines systems, behaviors, and interactions between them. It may also contain triggers and init blocks to control properties.

A core design concept behind the language is that things should be separate but composable.

Example

The following describes a model where one task sends messages and another task receives them.

// Define systems
SYSTEM: task_a = send*;     // system named "task_a" that has 0 or more "send" events
SYSTEM: task_b = receive*;  // system named "task_b" that has 0 or more "receive" events

// Describe interactions between systems
INTERACTION: task_a:send -> task_b:receive;  // task_a's send  then  task_b's receive

Systems

A system is a top-level behavior that marks where trace generation should start. It's a named pattern describing the expected events and / or behaviors.

Example system:

SYSTEM: sys = atomic_event behavior_pattern;

Behaviors

A behavior is like a system but not top-level. A system can reference a behavior. Use them to encapsulate complex system behaviors into simpler but more detailed building blocks.

Example behavior:

BEHAVIOR: behavior_pattern = expanded detail;

Patterns

A pattern defines expected events and / or behaviors. Used by systems, behaviors, and triggers. Also, provides the basis for selectors.

A pattern contains:

Type	Example	Meaning
sequences	a b	a then b
alternations	`a	b`
behaviors	behave	references a set of event behaviors defined elsewhere (a compound event)
events	event	an atomic event (like a behavior but without an expanded definition)
groups	`(a b	c)`
quantifiers	a+	a suffix that quantifies how many of leading thing should occur

Example patterns:

SYSTEM: sequence = a whitespace delimited list of events occurring in order;
SYSTEM: group = you can even (wrap stuff into groups);
SYSTEM: alternation = a (pipe | vertical bar | stick) delimited list of sequences;
BEHAVIOR: quantifiers = none_or_more* one_or_more+ none_or_one?;
BEHAVIOR: ranges = do_exactly_n_times{n} do_at_least_n_times{n,} do_n_to_m{n,m};

Interactions

An interaction relates two or more systems, and optionally enforces conditional requirements:

• relations:
  • a -> b (then) - orders events such that the traces will always result in a, then b
  • a == b (join) - joins systems together in the traces by treating a and b as the same event
• conditions:
  • { /* condition */ } system:thing (pre) - execute condition before the event; if it returns false, the trace is invalid at that event
  • system:thing { /* condition */ } (post) - execute condition after the event and its triggers; if it returns false, the trace is invalid at that event
• selectors (also in triggers):
  • system:pattern - patterns just like system and behavior definitions, but with a prepended system: describing where to look for the pattern

Example interactions:

INTERACTION: sys:before -> other_sys:after;
INTERACTION: sys:shared_event == other_sys:shared_event;
INTERACTION: { property > 5 } thing:happens_above_5 -> other_thing:stays_above_two { other_property >= 3 };

Triggers

A trigger is a chunk of code that will execute whenever the specified selector pattern occurs during trace generation.

Example trigger:

WHEN: sys:event1 event2 { SYSTEM.property++ };

Init blocks

An init block establishes the initial state of the model or a system through a code block.

Example init blocks:

INIT: { MODEL.initial_property = 5 };
INIT: system_a { SYSTEM.initial_property = 9001 };

Code Blocks

In their current form, the code blocks found in model-lang are embedded JavaScript.

They have access to different variables depending on what construct they are being used in.

The following table describes what the different types of code blocks have access to:

Type of Code Block Type	MODEL	SYSTEM	PREVIOUS	THIS
Conditionals (Interactions)	X
Init blocks	X	if given
Triggers	X	X	X	X

Scope variables:

• MODEL - contains information about the systems in the model
• SYSTEM - contains information about the events in the current system
• PREVIOUS - a reference to the previous node in the event trace
• THIS - a reference to the current node in the event trace

Misc

• Whitespace is insignificant.
• Comments are C-style.