Module eqc_fsm_esi

This is an Erlang Interface module between a simple Erlang web server (inets) and eqc_fsm.

Copyright © (C) 2015-2017, Quviq AB

Version: 1.42.1

Authors: Thomas Arts.

Description

This is an Erlang Interface module between a simple Erlang web server (inets) and eqc_fsm.

This module allows to use a browser for editing QuickCheck Finite State Machine specifications, in particular the states and their transitions. This requires an external tool, such as the graph editing tool developed in the Prowess research project.

QuickCheck eqc_fsm callback modules need to use the compiler directive that creates an external file representing the states, transitions and weights. This external file is then edited with a graph editing tool. In addition, testing results can be communicated to the graph editing tool to visualize these graphically.

This module is a ESI component as specified by Erlang inets. The idea is that one starts a webserver with inets:start(httpd, Options). To simplify this starting for the user, some start functions are provided in this module. The API calls that receive data from JavaScript deliver JSON data back to the server via esi_mod:deliver/2.

We communicate with Javascrit via JSON objects. One important object is the finite state machine graph with weighted transitions, a so called 'external_graph', since it represents the graph outside the eqc_fsm module. The string representation of the graph is defined according to the following grammar:

  graph -> "{" module "," "[" st_list "]" "}".
  module -> string.              %% callback module of eqc_fsm
  st_list -> st_element "," st_list.
  st_list -> st_element.
  st_element -> "{" state_name "," "[" tr_list "]" "}".
  state_name -> string.
  tr_list -> tr_element "," tr_list.
  tr_list -> tr_element.
  tr_element -> "{" state_name "," transition "," weight "}".
  transition -> string.
  weight -> string.           %% integer as string
  
Basically this representation makes it easy to parse the string as an Erlang term, since it is an Erlang term as a string. For example:
  {lock_eqc, {stopped, [{locked,[{locked,read,1},
                        {unlocked,unlock,1},
                        {locked,write,1},
                        {stopped,stop,1}]},
             {unlocked, [{unlocked,read,1},
                         {locked,lock,1},
                         {stopped,stop,1}]},
             {stopped, [{unlocked,start,1}]}]}}
  
Functions that expect a graph as input, do expect such a graph.

In order to use results of QuickCheck tests in the editor, the editor can retrieve for test results via eqc_fsm_esi. These tests results are generated by running QuickCheck on the property in the callback module. However, just running QuickCheck will not provide the results, the property must be enriched with the eqc_fsm_esi property combinator: aggregate_transitions/4.

A typlical eqc_fsm property then looks like:

   prop_fsm() ->
   ?FORALL(Cmds, commands(?MODULE),
   begin
     {H, S, Res} = run_commands(?MODULE,Cmds),
     pretty_commands(?MODULE, Cmds, {H, S, Res},
                     aggregate(command_names(Cmds),
                       eqc_fsm_esi:aggregate_transitions(?MODULE, Cmds, {H, S, Res},
                               Res == ok)))
   end).
   

Function Index

aggregate_transitions/4Transfer test statistics of eqc_fsm callback module Mod testing to eqc_fsm_esi.
esi_commands/3Called from JavaScript with the name of an eqc_fsm callback module.
esi_graph/3Called from JavaScript with the name of an eqc_fsm callback module.
esi_test_results/3Returns a graph structure containing the results of a test run.
esi_write_graph/3Called from JavaScript to update the state machine description for an eqc_fsm callback module.
esi_write_graph_without_weights/3Same as write_graph/3 but no weights function is created.
server_url/1Returns the URL to be called when starting a browser.
start/1Start an inets webserver to edit the graph for the eqc_fsm callback module: Module.
start/4Start an inets webserver on port Port to edit the graph for the eqc_fsm callback module: Module.
stop/1Stop the webserver for editing eqc_fsm state machines.

Function Details

aggregate_transitions/4

aggregate_transitions(Mod, Cmds, HSRes, Prop) -> any()

Transfer test statistics of eqc_fsm callback module Mod testing to eqc_fsm_esi.

esi_commands/3

esi_commands(Session::session(), X2::term(), Module::string()) -> json([string()])

Called from JavaScript with the name of an eqc_fsm callback module. Returns the commands defined by the eqc_fsm callback module: Module.

esi_graph/3

esi_graph(Session::session(), X2::term(), Module::string()) -> json(external_graph())

Called from JavaScript with the name of an eqc_fsm callback module. Returns the state machine description defined by the eqc_fsm callback module: Module. The returned graph has states, transitions and weights for each transition specified by eqc_fsm's type external_graph().

esi_test_results/3

esi_test_results(Session::session(), X2::term(), Module::string()) -> term()

Returns a graph structure containing the results of a test run

esi_write_graph/3

esi_write_graph(Session::session(), X::term(), Graph::string()) -> json(ok | error)

Called from JavaScript to update the state machine description for an eqc_fsm callback module. The graph is updated in the .fsm file associated with an eqc_fsm callback module and the code of the callback module is automatically recompiled and loaded. If the file could not be compiled or loaded, "error" is returned.

esi_write_graph_without_weights/3

esi_write_graph_without_weights(Session::session(), X::term(), Graph::string()) -> json(ok | error)

Same as write_graph/3 but no weights function is created. This can be useful if the weights are defined or should be defined in a different place.

server_url/1

server_url(Mod::moduel()) -> string()

Returns the URL to be called when starting a browser. If the server is not started, it returns "unknown".

start/1

start(Module::atom()) -> ok

Start an inets webserver to edit the graph for the eqc_fsm callback module: Module. In order to determine the root directory of the started webserver, i.e., where the html and JavaScript modules are stored, the application and OS environment variables are read. To set these variables use one of:

  application:set_env(eqc, eqc_webserver, PathToWebServerRoot).
  os:putenv("EQC_WEBSERVER", PathToWebServerRoot).
  
If both are defined, the OS environment takes precedence over the application environment.

The start command also starts a browser pointing to the toplevel html file that contains or points to the JavaScript accessing the API specified in eqc_fsm_esi. The name of the html file, or in fact, the path relative to the document root directory of the webserver (docs)) can be configured in a similar way:

  application:set_env(eqc, eqc_fsm_esi_html, HtmlFile).
  os:putenv("EQC_FSM_ESI_HTML", HtmlFile).
  
If both are defined, the OS environment takes precedence over the application environment. The URL pointing to the graph can be obtained using the server_url function.

start/4

start(Module::atom(), Port::integer(), Root::path(), Html::filename()) -> ok

Start an inets webserver on port Port to edit the graph for the eqc_fsm callback module: Module. Root specifies the root directory of the inets webserver, Html specifies the html file that contains or points to the JavaScript accessing the API specified in eqc_fsm_esi. It is a path relative to the document root of the server.

stop/1

stop(Mod) -> any()

Stop the webserver for editing eqc_fsm state machines.


Generated by EDoc, Sep 18 2017, 16:17:38.