1%%% -*- coding: utf-8; erlang-indent-level: 2 -*- 2%%% ------------------------------------------------------------------- 3%%% Copyright 2010-2021 Manolis Papadakis <manopapad@gmail.com>, 4%%% Eirini Arvaniti <eirinibob@gmail.com>, 5%%% and Kostis Sagonas <kostis@cs.ntua.gr> 6%%% 7%%% This file is part of PropEr. 8%%% 9%%% PropEr is free software: you can redistribute it and/or modify 10%%% it under the terms of the GNU General Public License as published by 11%%% the Free Software Foundation, either version 3 of the License, or 12%%% (at your option) any later version. 13%%% 14%%% PropEr is distributed in the hope that it will be useful, 15%%% but WITHOUT ANY WARRANTY; without even the implied warranty of 16%%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 17%%% GNU General Public License for more details. 18%%% 19%%% You should have received a copy of the GNU General Public License 20%%% along with PropEr. If not, see <http://www.gnu.org/licenses/>. 21 22%%% @copyright 2010-2021 Manolis Papadakis, Eirini Arvaniti, and Kostis Sagonas 23%%% @version {@version} 24%%% @author Eirini Arvaniti 25 26%%% @doc This module defines the `proper_fsm' behaviour, useful for testing 27%%% systems that can be modeled as finite state machines. That is, a finite 28%%% collection of named states and transitions between them. `{@module}' is 29%%% closely related to {@link proper_statem} and is, in fact, implemented in 30%%% terms of that. Testcases generated using `{@module}' will be on precisely 31%%% the same form as testcases generated using {@link proper_statem}. The 32%%% difference lies in the way the callback modules are specified. 33%%% The relation between {@link proper_statem} and `{@module}' is similar 34%%% to the one between `gen_server' and `gen_fsm' in OTP libraries. 35%%% 36%%% Due to name conflicts with functions automatically imported from 37%%% {@link proper_statem}, a fully qualified call is needed in order to 38%%% use the <a href="#index">API functions </a> of `{@module}'. 39%%% 40%%% === The states of the finite state machine === 41%%% Following the convention used in `gen_fsm behaviour', the state is 42%%% separated into a `StateName::'{@type state_name()} and some 43%%% `StateData::'{@type state_data()}. `StateName' is used to denote a state 44%%% of the finite state machine and `StateData' is any relevant information 45%%% that has to be stored in the model state. States are fully 46%%% represented as tuples `{StateName, StateData}'. 47%%% 48%%% `StateName' is usually an atom (i.e. the name of the state), but can also 49%%% be a tuple. In the latter case, the first element of the tuple must be an 50%%% atom specifying the name of the state, whereas the rest of the elements can 51%%% be arbitrary terms specifying state attributes. For example, when 52%%% implementing the fsm of an elevator which can reach N different floors, the 53%%% `StateName' for each floor could be `{floor,K}, 1 <= K <= N'.<br/> 54%%% `StateData' can be an arbitrary term, but is usually a record. 55%%% 56%%% === Transitions between states === 57%%% A transition ({@type transition()}) is represented as a tuple 58%%% `{TargetState, {call,M,F,A}}'. This means that performing the specified 59%%% symbolic call at the current state of the fsm will lead to `TargetState'. 60%%% The atom `history' can be used as `TargetState' to denote that a transition 61%%% does not change the current state of the fsm. 62%%% 63%%% === The callback functions === 64%%% The following functions must be exported from the callback module 65%%% implementing the finite state machine: 66%%% <ul> 67%%% <li> `initial_state() ->' {@type state_name()} 68%%% <p>Specifies the initial state of the finite state machine. As with 69%%% `proper_statem:initial_state/0', its result should be deterministic. 70%%% </p></li> 71%%% <li> `initial_state_data() ->' {@type state_data()} 72%%% <p>Specifies what the state data should initially contain. Its result 73%%% should be deterministic</p></li> 74%%% <li> `StateName(S::'{@type state_data()}`) ->' 75%%% `['{@type transition()}`]' 76%%% <p>There should be one instance of this function for each reachable 77%%% state `StateName' of the finite state machine. In case `StateName' is a 78%%% tuple the function takes a different form, described just below. The 79%%% function returns a list of possible transitions ({@type transition()}) 80%%% from the current state. 81%%% At command generation time, the instance of this function with the same 82%%% name as the current state's name is called to return the list of possible 83%%% transitions. Then, PropEr will randomly choose a transition and, 84%%% according to that, generate the next symbolic call to be included in the 85%%% command sequence. However, before the call is actually included, a 86%%% precondition that might impose constraints on `StateData' is checked.<br/> 87%%% Note also that PropEr detects transitions that would raise an exception 88%%% of class `<error>' at generation time (not earlier) and does not choose 89%%% them. This feature can be used to include conditional transitions that 90%%% depend on the `StateData'.</p></li> 91%%% <li> `StateName(Attr1::term(), ..., AttrN::term(), 92%%% S::'{@type state_data()}`) ->' 93%%% `['{@type transition()}`]' 94%%% <p>There should be one instance of this function for each reachable state 95%%% `{StateName,Attr1,...,AttrN}' of the finite state machine. The function 96%%% has similar beaviour to `StateName/1', described above.</p></li> 97%%% <li> `weight(From::'{@type state_name()}`, 98%%% Target::'{@type state_name()}`, 99%%% Call::'{@type symbolic_call()}`) -> non_neg_integer()' 100%%% <p>This is an optional callback. When it is not defined (or not exported), 101%%% transitions are chosen with equal probability. When it is defined, it 102%%% assigns a non-negative integer weight to transitions from `From' to `Target' 103%%% triggered by symbolic call `Call'. In this case, each transition is chosen 104%%% with probability proportional to the weight assigned.</p></li> 105%%% <li> `precondition(From::'{@type state_name()}`, 106%%% Target::'{@type state_name()}`, 107%%% StateData::'{@type state_data()}`, 108%%% Call::'{@type symbolic_call()}`) -> boolean()' 109%%% <p>Similar to `proper_statem:precondition/2'. Specifies the 110%%% precondition that should hold about `StateData' so that `Call' can be 111%%% included in the command sequence. In case precondition doesn't hold, a 112%%% new transition is chosen using the appropriate `StateName/1' generator. 113%%% It is possible for more than one transitions to be triggered by the same 114%%% symbolic call and lead to different target states. In this case, at most 115%%% one of the target states may have a true precondition. Otherwise, PropEr 116%%% will not be able to detect which transition was chosen and an exception 117%%% will be raised.</p></li> 118%%% <li> `postcondition(From::'{@type state_name()}`, 119%%% Target::'{@type state_name()}`, 120%%% StateData::'{@type state_data()}`, 121%%% Call::'{@type symbolic_call()}`, 122%%% Res::'{@type cmd_result()}`) -> boolean()' 123%%% <p>Similar to `proper_statem:postcondition/3'. Specifies the 124%%% postcondition that should hold about the result `Res' of the evaluation 125%%% of `Call'.</p></li> 126%%% <li> `next_state_data(From::'{@type state_name()}`, 127%%% Target::'{@type state_name()}`, 128%%% StateData::'{@type state_data()}`, 129%%% Res::'{@type cmd_result()}`, 130%%% Call::'{@type symbolic_call()}`) ->' 131%%% {@type state_data()} 132%%% <p>Similar to `proper_statem:next_state/3'. Specifies how the 133%%% transition from `FromState' to `Target' triggered by `Call' affects the 134%%% `StateData'. `Res' refers to the result of `Call' and can be either 135%%% symbolic or dynamic.</p></li> 136%%% </ul> 137%%% 138%%% === The property used === 139%%% This is an example of a property that can be used to test a 140%%% finite state machine specification: 141%%% 142%%% ```prop_fsm() -> 143%%% ?FORALL(Cmds, proper_fsm:commands(?MODULE), 144%%% begin 145%%% {_History, _State, Result} = proper_fsm:run_commands(?MODULE, Cmds), 146%%% cleanup(), 147%%% Result =:= ok 148%%% end).''' 149%%% 150%%% == Stateful Targeted Testing == 151%%% During testing of the system's behavior, there may be some failing command 152%%% sequences that the random property based testing does not find with ease, 153%%% or at all. In these cases, stateful targeted property based testing can help 154%%% find such edge cases, provided a utility value. 155%%% 156%%% ```prop_targeted_testing() -> 157%%% ?FORALL_TARGETED(Cmds, proper_fsm:commands(?MODULE), 158%%% begin 159%%% {History, State, Result} = proper_fsm:run_commands(?MODULE, Cmds), 160%%% UV = uv(History, State, Result), 161%%% ?MAXIMIZE(UV), 162%%% cleanup(), 163%%% Result =:= ok 164%%% end).''' 165%%% 166%%% Νote that the `UV' value can be computed in any way fit, depending on the 167%%% use case. `uv/3' is used here as a dummy function which computes the 168%%% utility value. 169%%% @end 170 171-module(proper_fsm). 172 173-export([commands/1, commands/2, run_commands/2, run_commands/3, 174 state_names/1]). 175-export([command/1, precondition/2, next_state/3, postcondition/3]). 176-export([target_states/4]). 177 178-include("proper_internal.hrl"). 179 180 181%% ----------------------------------------------------------------------------- 182%% Type declarations 183%% ----------------------------------------------------------------------------- 184 185-type symbolic_var() :: proper_statem:symbolic_var(). 186-type symbolic_call():: proper_statem:symbolic_call(). 187-type fsm_result() :: proper_statem:statem_result(). 188-type state_name() :: atom() | tuple(). 189-type state_data() :: term(). 190-type fsm_state() :: {state_name(),state_data()}. 191-type transition() :: {state_name(),symbolic_call()}. 192-type command() :: {'set',symbolic_var(),symbolic_call()} 193 | {'init',fsm_state()}. 194-type command_list() :: [command()]. 195-type cmd_result() :: term(). 196-type history() :: [{fsm_state(),cmd_result()}]. 197-type tmp_command() :: {'init',state()} 198 | {'set',symbolic_var(),symbolic_call()}. 199 200-record(state, {name :: state_name(), 201 data :: state_data(), 202 mod :: mod_name()}). 203-type state() :: #state{}. 204 205 206%% ----------------------------------------------------------------------------- 207%% Proper_fsm behaviour callback functions 208%% ----------------------------------------------------------------------------- 209 210-callback initial_state() -> state_name(). 211 212-callback initial_state_data() -> state_data(). 213 214-callback precondition(state_name(), state_name(), 215 state_data(), symbolic_call()) -> boolean(). 216 217-callback postcondition(state_name(), state_name(), state_data(), 218 symbolic_call(), cmd_result()) -> boolean(). 219 220-callback next_state_data(state_name(), state_name(), state_data(), 221 cmd_result(), symbolic_call()) -> state_data(). 222 223-callback weight(state_name(), state_name(), symbolic_call()) -> non_neg_integer(). 224 225-optional_callbacks([weight/3]). 226 227 228%% ----------------------------------------------------------------------------- 229%% API 230%% ----------------------------------------------------------------------------- 231 232%% @doc A special PropEr type which generates random command sequences, 233%% according to a finite state machine specification. The function takes as 234%% input the name of a callback module, which contains the fsm specification. 235%% The initial state is computed by <br/> 236%% `{Mod:initial_state/0, Mod:initial_state_data/0}'. 237 238-spec commands(mod_name()) -> proper_types:type(). 239commands(Mod) -> 240 ?USERNF(commands_gen(Mod), next_commands_gen(Mod)). 241 242-spec commands_gen(mod_name()) -> proper_types:type(). 243commands_gen(Mod) -> 244 ?LET([_|Cmds], 245 proper_statem:commands_gen(?MODULE, initial_state(Mod)), 246 Cmds). 247 248%% @doc Similar to {@link commands/1}, but generated command sequences always 249%% start at a given state. In this case, the first command is always <br/> 250%% `{init, InitialState = {Name,Data}}' and is used to correctly initialize the 251%% state every time the command sequence is run (i.e. during normal execution, 252%% while shrinking and when checking a counterexample). 253 254-spec commands(mod_name(), fsm_state()) -> proper_types:type(). 255commands(Mod, InitialState) -> 256 ?USERNF(commands_gen(Mod, InitialState), 257 next_commands_gen(Mod, InitialState)). 258 259-spec commands_gen(mod_name(), fsm_state()) -> proper_types:type(). 260commands_gen(Mod, {Name,Data} = InitialState) -> 261 State = #state{name = Name, data = Data, mod = Mod}, 262 ?LET([_|Cmds], 263 proper_statem:commands_gen(?MODULE, State), 264 [{init,InitialState}|Cmds]). 265 266next_commands_gen(Mod) -> 267 InitialState = initial_state(Mod), 268 StatemNext = proper_statem:next_commands_gen(?MODULE, InitialState), 269 fun (Cmds, {Depth, Temp}) -> 270 ?LET([_ | NextCmds], StatemNext(Cmds, {Depth, Temp}), NextCmds) 271 end. 272 273next_commands_gen(Mod, {Name, Data} = InitialState) -> 274 State = #state{name = Name, data = Data, mod = Mod}, 275 StatemNext = proper_statem:next_commands_gen(?MODULE, State), 276 fun (Cmds, {Depth, Temp}) -> 277 ?LET([_ | NextCmds], StatemNext(Cmds, {Depth, Temp}), 278 [{init, InitialState} | NextCmds]) 279 end. 280 281%% @doc Evaluates a given symbolic command sequence `Cmds' according to the 282%% finite state machine specified in `Mod'. The result is a triple of the 283%% form<br/> `{History, FsmState, Result}', similar to 284%% {@link proper_statem:run_commands/2}. 285 286-spec run_commands(mod_name(), command_list()) -> 287 {history(),fsm_state(),fsm_result()}. 288run_commands(Mod, Cmds) -> 289 run_commands(Mod, Cmds, []). 290 291%% @doc Similar to {@link run_commands/2}, but also accepts an environment 292%% used for symbolic variable evaluation, exactly as described in 293%% {@link proper_statem:run_commands/3}. 294 295-spec run_commands(mod_name(), command_list(), proper_symb:var_values()) -> 296 {history(),fsm_state(),fsm_result()}. 297run_commands(Mod, Cmds, Env) -> 298 Cmds1 = tmp_commands(Mod, Cmds), 299 {H,S,Res} = proper_statem:run_commands(?MODULE, Cmds1, Env), 300 History = [{{Name,Data},R} || {#state{name = Name, data = Data},R} <- H], 301 State = {S#state.name, S#state.data}, 302 {History, State, Res}. 303 304%% @doc Extracts the names of the states from a given command execution history. 305%% It is useful in combination with functions such as {@link proper:aggregate/2} 306%% in order to collect statistics about state transitions during command 307%% execution. 308 309-spec state_names(history()) -> [state_name()]. 310state_names(History) -> 311 [SName || {{SName,_},_Res} <- History]. 312 313 314%% ----------------------------------------------------------------------------- 315%% Proper_statem bahaviour callback functions 316%% ----------------------------------------------------------------------------- 317 318-spec initial_state(mod_name()) -> state(). 319initial_state(Mod) -> 320 S_name = Mod:initial_state(), 321 S_data = Mod:initial_state_data(), 322 #state{name = S_name, data = S_data, mod = Mod}. 323 324%% @private 325-spec command(state()) -> proper_types:type(). 326command(#state{name = From, data = Data, mod = Mod}) -> 327 choose_transition(Mod, From, get_transitions(Mod, From, Data)). 328 329%% @private 330-spec precondition(state(), symbolic_call()) -> boolean(). 331precondition(#state{name = From, data = Data, mod = Mod}, Call) -> 332 Targets = target_states(Mod, From, Data, Call), 333 case [To || To <- Targets, 334 Mod:precondition(From, cook_history(From, To), Data, Call)] of 335 [] -> 336 false; 337 [_T] -> 338 true; 339 _ -> 340 io:format( 341 "~nError: The transition from \"~w\" state triggered by ~w " 342 "call leads to multiple target states.~nUse the precondition/5 " 343 "callback to specify which target state should be chosen.~n", 344 [From, get_mfa(Call)]), 345 erlang:error(too_many_targets) 346 end. 347 348%% @private 349-spec next_state(state(), symbolic_var() | cmd_result(), symbolic_call()) -> state(). 350next_state(S = #state{name = From, data = Data, mod = Mod} , Var, Call) -> 351 To = cook_history(From, transition_target(Mod, From, Data, Call)), 352 S#state{name = To, 353 data = Mod:next_state_data(From, To, Data, Var, Call)}. 354 355%% @private 356-spec postcondition(state(), symbolic_call(), cmd_result()) -> boolean(). 357postcondition(#state{name = From, data = Data, mod = Mod}, Call, Res) -> 358 To = cook_history(From, transition_target(Mod, From, Data, Call)), 359 Mod:postcondition(From, To, Data, Call, Res). 360 361 362%% ----------------------------------------------------------------------------- 363%% Utility functions 364%% ----------------------------------------------------------------------------- 365 366-spec tmp_commands(mod_name(), command_list()) -> [tmp_command()]. 367tmp_commands(Mod, Cmds) -> 368 case Cmds of 369 [{init, {Name,Data}}|Rest] -> 370 I = #state{name = Name, data = Data, mod = Mod}, 371 [{init,I}|Rest]; 372 Rest -> 373 I = initial_state(Mod), 374 [{init,I}|Rest] 375 end. 376 377-spec get_transitions(mod_name(), state_name(), state_data()) -> 378 [transition()]. 379get_transitions(Mod, StateName, Data) -> 380 case StateName of 381 From when is_atom(From) -> 382 Mod:From(Data); 383 From when is_tuple(From) -> 384 Fun = element(1, From), 385 Args = tl(tuple_to_list(From)), 386 apply(Mod, Fun, Args ++ [Data]) 387 end. 388 389-spec choose_transition(mod_name(), state_name(), [transition()]) -> 390 proper_types:type(). 391choose_transition(Mod, From, T_list) -> 392 case is_exported(Mod, {weight,3}) of 393 false -> 394 choose_uniform_transition(T_list); 395 true -> 396 choose_weighted_transition(Mod, From, T_list) 397 end. 398 399-spec choose_uniform_transition([transition()]) -> proper_types:type(). 400choose_uniform_transition(T_list) -> 401 List = [CallGen || {_,CallGen} <- T_list], 402 proper_types:safe_union(List). 403 404-spec choose_weighted_transition(mod_name(), state_name(), [transition()]) -> 405 proper_types:type(). 406choose_weighted_transition(Mod, From, T_list) -> 407 List = [{Mod:weight(From, cook_history(From, To), CallGen), CallGen} 408 || {To,CallGen} <- T_list], 409 proper_types:safe_weighted_union(List). 410 411-spec cook_history(state_name(), state_name()) -> state_name(). 412cook_history(From, history) -> From; 413cook_history(_, To) -> To. 414 415-spec is_exported(mod_name(), {fun_name(),arity()}) -> boolean(). 416is_exported(Mod, Fun) -> 417 lists:member(Fun, Mod:module_info(exports)). 418 419-spec transition_target(mod_name(), state_name(), state_data(), symbolic_call()) -> 420 state_name(). 421transition_target(Mod, From, Data, Call) -> 422 Targets = target_states(Mod, From, Data, Call), 423 [To] = [T || T <- Targets, 424 Mod:precondition(From, cook_history(From, T), Data, Call)], 425 To. 426 427%% @private 428-spec target_states(mod_name(), state_name(), state_data(), symbolic_call()) -> 429 [state_name()]. 430target_states(Mod, From, StateData, Call) -> 431 find_target(get_transitions(Mod, From, StateData), Call, []). 432 433-spec find_target([transition()], symbolic_call(), [state_name()]) -> 434 [state_name()]. 435find_target([], _, Accum) -> Accum; 436find_target(Transitions, Call, Accum) -> 437 [{Target,CallGen}|Rest] = Transitions, 438 case is_compatible(Call, CallGen) of 439 true -> find_target(Rest, Call, [Target|Accum]); 440 false -> find_target(Rest, Call, Accum) 441 end. 442 443-spec is_compatible(symbolic_call(), symbolic_call()) -> boolean(). 444is_compatible({call,M,F,A1}, {call,M,F,A2}) 445 when length(A1) =:= length(A2) -> 446 true; 447is_compatible(_, _) -> 448 false. 449 450-spec get_mfa(symbolic_call()) -> mfa(). 451get_mfa({call,M,F,A}) -> {M,F,length(A)}. 452