From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!not-for-mail From: Leo Liu Newsgroups: gmane.emacs.bugs Subject: bug#24012: 25.0.95; forward-comment backwards takes O(n^2) Date: Sun, 17 Jul 2016 19:04:18 +0800 Message-ID: NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: multipart/mixed; boundary="=-=-=" X-Trace: ger.gmane.org 1468753531 18804 80.91.229.3 (17 Jul 2016 11:05:31 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Sun, 17 Jul 2016 11:05:31 +0000 (UTC) To: 24012@debbugs.gnu.org Original-X-From: bug-gnu-emacs-bounces+geb-bug-gnu-emacs=m.gmane.org@gnu.org Sun Jul 17 13:05:21 2016 Return-path: Envelope-to: geb-bug-gnu-emacs@m.gmane.org Original-Received: from lists.gnu.org ([208.118.235.17]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1bOjsr-0001ku-Vm for geb-bug-gnu-emacs@m.gmane.org; Sun, 17 Jul 2016 13:05:18 +0200 Original-Received: from localhost ([::1]:40970 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1bOjsr-0001zL-06 for geb-bug-gnu-emacs@m.gmane.org; Sun, 17 Jul 2016 07:05:17 -0400 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:59727) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1bOjsh-0001ub-1b for bug-gnu-emacs@gnu.org; Sun, 17 Jul 2016 07:05:10 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1bOjsc-0001XP-NJ for bug-gnu-emacs@gnu.org; Sun, 17 Jul 2016 07:05:05 -0400 Original-Received: from debbugs.gnu.org ([208.118.235.43]:41962) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1bOjsc-0001XL-Ji for bug-gnu-emacs@gnu.org; Sun, 17 Jul 2016 07:05:02 -0400 Original-Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1bOjsc-0008QP-DW for bug-gnu-emacs@gnu.org; Sun, 17 Jul 2016 07:05:02 -0400 X-Loop: help-debbugs@gnu.org Resent-From: Leo Liu Original-Sender: "Debbugs-submit" Resent-CC: bug-gnu-emacs@gnu.org Resent-Date: Sun, 17 Jul 2016 11:05:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: report 24012 X-GNU-PR-Package: emacs X-GNU-PR-Keywords: X-Debbugs-Original-To: bug-gnu-emacs@gnu.org Original-Received: via spool by submit@debbugs.gnu.org id=B.146875349232365 (code B ref -1); Sun, 17 Jul 2016 11:05:02 +0000 Original-Received: (at submit) by debbugs.gnu.org; 17 Jul 2016 11:04:52 +0000 Original-Received: from localhost ([127.0.0.1]:54299 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1bOjsQ-0008Pw-Vv for submit@debbugs.gnu.org; Sun, 17 Jul 2016 07:04:51 -0400 Original-Received: from eggs.gnu.org ([208.118.235.92]:40493) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1bOjsO-0008Pf-0I for submit@debbugs.gnu.org; Sun, 17 Jul 2016 07:04:49 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1bOjsF-0001U4-OG for submit@debbugs.gnu.org; Sun, 17 Jul 2016 07:04:42 -0400 Original-Received: from lists.gnu.org ([2001:4830:134:3::11]:49556) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1bOjsF-0001Tz-L7 for submit@debbugs.gnu.org; Sun, 17 Jul 2016 07:04:39 -0400 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:59684) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1bOjs9-0001FS-SH for bug-gnu-emacs@gnu.org; Sun, 17 Jul 2016 07:04:37 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1bOjs5-0001TG-HQ for bug-gnu-emacs@gnu.org; Sun, 17 Jul 2016 07:04:32 -0400 Original-Received: from mail-wm0-x233.google.com ([2a00:1450:400c:c09::233]:36684) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1bOjs5-0001T3-3Q for bug-gnu-emacs@gnu.org; Sun, 17 Jul 2016 07:04:29 -0400 Original-Received: by mail-wm0-x233.google.com with SMTP id f126so73166171wma.1 for ; Sun, 17 Jul 2016 04:04:27 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=from:to:subject:date:message-id:mime-version; bh=NPUpGcLPsFPndfxAF3acewPDKWQGI2hcCSAcvVk80r8=; b=mnldLJx6Ix/CVpM9BaQMJqJUtxSrwkr2HV/1pK0E/5uXUwfTNGkqi3+8dBAg9G1URJ CPARbfPW07HIx+tyLGrALaZ+Mhdu5A2rct9h5SrFtbybXEYUDM+z4RxS2WHzsU2jaTMt 2bqsuKLFH4yHWs26YVyha3SDA3gz2Hofnga8KN3Zo68A6AvhhkLtMfCV4Ypsq38oM6AH fLT9vPwZ498i/zGKAX2i4n8zPqB1W4yOYqKoH9hdEo5sKNua54or4uhq/I38mm8/3MZ0 N/oprmdWA2x8cXsx0xG4SFLK2aHL6i4jZDwp4qc6bKblh/ltZk0s+Xi8KYUP4fTjO2fx qV0Q== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:from:to:subject:date:message-id:mime-version; bh=NPUpGcLPsFPndfxAF3acewPDKWQGI2hcCSAcvVk80r8=; b=DCwif5TFOmynnN83wSCC650/g6F3HKuTTBGNHKnrt49mmnairh6aQbx/Rn+akKmkYS x5Y3rqvqhKd3OoMylV54yhi8ReZAcGRREipG0pw+rPJroycSwgIknmKJ7Kof1yM4INc8 xaHqvYtCACgZ7alBFlIC5ja+hp5Ft7N3GF4KOBDT+t56jirKw5lvngf5ev8UUW9xu1tB UnyKYzrrvUmySYdZKiNbn2PEHQHK1RUioeLx4LAJsDQr+BWiYNcHoSkPrIdC2qh/z7Kf 89tCra076siDv5aZWiw/5Dxz2uG/b9dp9SwHSviGr8h0A6m6/HAAq/DPddNWJ9h7Xar4 BtKg== X-Gm-Message-State: ALyK8tKUD0g9L/F0hakcHAeDb7J2U1mV12ytjgIHUUUy5+Pfn5wIXNx3cDWkVVz7oO1rZQ== X-Received: by 10.28.225.4 with SMTP id y4mr31322953wmg.98.1468753466816; Sun, 17 Jul 2016 04:04:26 -0700 (PDT) Original-Received: from zeuss-MacBook-Pro.local ([46.101.90.246]) by smtp.gmail.com with ESMTPSA id i195sm8298058wmg.1.2016.07.17.04.04.23 for (version=TLS1_2 cipher=ECDHE-RSA-CHACHA20-POLY1305 bits=256/256); Sun, 17 Jul 2016 04:04:25 -0700 (PDT) X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.6.x X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 208.118.235.43 X-BeenThere: bug-gnu-emacs@gnu.org List-Id: "Bug reports for GNU Emacs, the Swiss army knife of text editors" List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: bug-gnu-emacs-bounces+geb-bug-gnu-emacs=m.gmane.org@gnu.org Original-Sender: "bug-gnu-emacs" Xref: news.gmane.org gmane.emacs.bugs:121163 Archived-At: --=-=-= Content-Type: text/plain 1. Use the attached file as an example, open it in emacs in ruby-mode 2. Move point to end of buffer and eval (forward-comment (- (point))) The last step takes about 0.25 seconds on my MacBook 3 GHz Intel Core i7. If you double the lines of comments, the time increase by 4 folds. Any idea why forward-comment backwards is so slow? Leo --=-=-= Content-Type: text/plain Content-Disposition: attachment; filename=tt.rb Content-Description: tt.rb ### PropEr is free software: you can redistribute it and/or modify ### it under the terms of the GNU General Public License as published by ### the Free Software Foundation, either version 3 of the License, or ### (at your option) any later version. ### ### PropEr is distributed in the hope that it will be useful, ### but WITHOUT ANY WARRANTY; without even the implied warranty of ### MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the ### GNU General Public License for more details. ### ### You should have received a copy of the GNU General Public License ### along with PropEr. If not, see . ### @copyright 2010-2016 Manolis Papadakis, Eirini Arvaniti and Kostis Sagonas ### @version {@version} ### @author Eirini Arvaniti ### @doc This module defines the `proper_fsm' behaviour, useful for testing ### systems that can be modeled as finite state machines. That is, a finite ### collection of named states and transitions between them. `{@module}' is ### closely related to {@link proper_statem} and is, in fact, implemented in ### terms of that. Testcases generated using `{@module}' will be on precisely ### the same form as testcases generated using {@link proper_statem}. The ### difference lies in the way the callback modules are specified. ### The relation between {@link proper_statem} and `{@module}' is similar ### to the one between `gen_server' and `gen_fsm' in OTP libraries. ### ### Due to name conflicts with functions automatically imported from ### {@link proper_statem}, a fully qualified call is needed in order to ### use the API functions of `{@module}'. ### ### === The states of the finite state machine === ### Following the convention used in `gen_fsm behaviour', the state is ### separated into a `StateName::'{@type state_name()} and some ### `StateData::'{@type state_data()}. `StateName' is used to denote a state ### of the finite state machine and `StateData' is any relevant information ### that has to be stored in the model state. States are fully ### represented as tuples `{StateName, StateData}'. ### ### `StateName' is usually an atom (i.e. the name of the state), but can also ### be a tuple. In the latter case, the first element of the tuple must be an ### atom specifying the name of the state, whereas the rest of the elements can ### be arbitrary terms specifying state attributes. For example, when ### implementing the fsm of an elevator which can reach N different floors, the ### `StateName' for each floor could be `{floor,K}, 1 <= K <= N'.
### `StateData' can be an arbitrary term, but is usually a record. ### ### === Transitions between states === ### A transition ({@type transition()}) is represented as a tuple ### `{TargetState, {call,M,F,A}}'. This means that performing the specified ### symbolic call at the current state of the fsm will lead to `TargetState'. ### The atom `history' can be used as `TargetState' to denote that a transition ### does not change the current state of the fsm. ### ### === The callback functions === ### The following functions must be exported from the callback module ### implementing the finite state machine: ###
    ###
  • `initial_state() ->' {@type state_name()} ###

    Specifies the initial state of the finite state machine. As with ### `proper_statem:initial_state/0', its result should be deterministic. ###

    • ###
  • `initial_state_data() ::' {@type state_data()} ###

    Specifies what the state data should initially contain. Its result ### should be deterministic

    • ###
  • `StateName(S::'{@type state_data()}`) ::' ### `['{@type transition()}`]' ###

    There should be one instance of this function for each reachable ### state `StateName' of the finite state machine. In case `StateName' is a ### tuple the function takes a different form, described just below. The ### function returns a list of possible transitions ({@type transition()}) ### from the current state. ### At command generation time, the instance of this function with the same ### name as the current state's name is called to return the list of possible ### transitions. Then, PropEr will randomly choose a transition and, ### according to that, generate the next symbolic call to be included in the ### command sequence. However, before the call is actually included, a ### precondition that might impose constraints on `StateData' is checked.
    ### Note also that PropEr detects transitions that would raise an exception ### of class `' at generation time (not earlier) and does not choose ### them. This feature can be used to include conditional transitions that ### depend on the `StateData'.

    • ###
  • `StateName(Attr1::term(), ..., AttrN::term(), ### S::'{@type state_data()}`) ::' ### `['{@type transition()}`]' ###

    There should be one instance of this function for each reachable state ### `{StateName,Attr1,...,AttrN}' of the finite state machine. The function ### has similar beaviour to `StateName/1', described above.

    • ###
  • `weight(From::'{@type state_name()}`, ### Target::'{@type state_name()}`, ### Call::'{@type symbolic_call()}`) -> integer()' ###

    This is an optional callback. When it is not defined (or not exported), ### transitions are chosen with equal probability. When it is defined, it ### assigns an integer weight to transitions from `From' to `Target' ### triggered by symbolic call `Call'. In this case, each transition is chosen ### with probability proportional to the weight assigned.

    • ###
  • `precondition(From::'{@type state_name()}`, ### Target::'{@type state_name()}`, ### StateData::'{@type state_data()}`, ### Call::'{@type symbolic_call()}`) -> boolean()' ###

    Similar to `proper_statem:precondition/2'. Specifies the ### precondition that should hold about `StateData' so that `Call' can be ### included in the command sequence. In case precondition doesn't hold, a ### new transition is chosen using the appropriate `StateName/1' generator. ### It is possible for more than one transitions to be triggered by the same ### symbolic call and lead to different target states. In this case, at most ### one of the target states may have a true precondition. Otherwise, PropEr ### will not be able to detect which transition was chosen and an exception ### will be raised.

    • ###
  • `postcondition(From::'{@type state_name()}`, ### Target::'{@type state_name()}`, ### StateData::'{@type state_data()}`, ### Call::'{@type symbolic_call()}`, ### Res::'{@type cmd_result()}`) -> boolean()' ###

    Similar to `proper_statem:postcondition/3'. Specifies the ### postcondition that should hold about the result `Res' of the evaluation ### of `Call'.

    • ###
  • `next_state_data(From::'{@type state_name()}`, ### Target::'{@type state_name()}`, ### StateData::'{@type state_data()}`, ### Res::'{@type cmd_result()}`, ### Call::'{@type symbolic_call()}`) ->' ### {@type state_data()} ###

    Similar to `proper_statem:next_state/3'. Specifies how the ### transition from `FromState' to `Target' triggered by `Call' affects the ### `StateData'. `Res' refers to the result of `Call' and can be either ### symbolic or dynamic.

    • ###
### ### === The property used === ### This is an example of a property that can be used to test a ### finite state machine specification: ### ### ```prop_fsm() -> ### ?FORALL(Cmds, proper_fsm:commands(?MODULE), ### begin ### {_History, _State, Result} = proper_fsm:run_commands(?MODULE, Cmds), ### cleanup(), ### Result =:= ok ### end).''' ### @end ### Copyright 2010-2016 Manolis Papadakis , ### Eirini Arvaniti ### and Kostis Sagonas ### ### This file is part of PropEr. ### ### PropEr is free software: you can redistribute it and/or modify ### it under the terms of the GNU General Public License as published by ### the Free Software Foundation, either version 3 of the License, or ### (at your option) any later version. ### ### PropEr is distributed in the hope that it will be useful, ### but WITHOUT ANY WARRANTY; without even the implied warranty of ### MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the ### GNU General Public License for more details. ### ### You should have received a copy of the GNU General Public License ### along with PropEr. If not, see . ### @copyright 2010-2016 Manolis Papadakis, Eirini Arvaniti and Kostis Sagonas ### @version {@version} ### @author Eirini Arvaniti ### @doc This module defines the `proper_fsm' behaviour, useful for testing ### systems that can be modeled as finite state machines. That is, a finite ### collection of named states and transitions between them. `{@module}' is ### closely related to {@link proper_statem} and is, in fact, implemented in ### terms of that. Testcases generated using `{@module}' will be on precisely ### the same form as testcases generated using {@link proper_statem}. The ### difference lies in the way the callback modules are specified. ### The relation between {@link proper_statem} and `{@module}' is similar ### to the one between `gen_server' and `gen_fsm' in OTP libraries. ### ### Due to name conflicts with functions automatically imported from ### {@link proper_statem}, a fully qualified call is needed in order to ### use the API functions of `{@module}'. ### ### === The states of the finite state machine === ### Following the convention used in `gen_fsm behaviour', the state is ### separated into a `StateName::'{@type state_name()} and some ### `StateData::'{@type state_data()}. `StateName' is used to denote a state ### of the finite state machine and `StateData' is any relevant information ### that has to be stored in the model state. States are fully ### represented as tuples `{StateName, StateData}'. ### ### `StateName' is usually an atom (i.e. the name of the state), but can also ### be a tuple. In the latter case, the first element of the tuple must be an ### atom specifying the name of the state, whereas the rest of the elements can ### be arbitrary terms specifying state attributes. For example, when ### implementing the fsm of an elevator which can reach N different floors, the ### `StateName' for each floor could be `{floor,K}, 1 <= K <= N'.
### `StateData' can be an arbitrary term, but is usually a record. ### ### === Transitions between states === ### A transition ({@type transition()}) is represented as a tuple ### `{TargetState, {call,M,F,A}}'. This means that performing the specified ### symbolic call at the current state of the fsm will lead to `TargetState'. ### The atom `history' can be used as `TargetState' to denote that a transition ### does not change the current state of the fsm. ### ### === The callback functions === ### The following functions must be exported from the callback module ### implementing the finite state machine: ###
    ###
  • `initial_state() ->' {@type state_name()} ###

    Specifies the initial state of the finite state machine. As with ### `proper_statem:initial_state/0', its result should be deterministic. ###

    • ###
  • `initial_state_data() ::' {@type state_data()} ###

    Specifies what the state data should initially contain. Its result ### should be deterministic

    • ###
  • `StateName(S::'{@type state_data()}`) ::' ### `['{@type transition()}`]' ###

    There should be one instance of this function for each reachable ### state `StateName' of the finite state machine. In case `StateName' is a ### tuple the function takes a different form, described just below. The ### function returns a list of possible transitions ({@type transition()}) ### from the current state. ### At command generation time, the instance of this function with the same ### name as the current state's name is called to return the list of possible ### transitions. Then, PropEr will randomly choose a transition and, ### according to that, generate the next symbolic call to be included in the ### command sequence. However, before the call is actually included, a ### precondition that might impose constraints on `StateData' is checked.
    ### Note also that PropEr detects transitions that would raise an exception ### of class `' at generation time (not earlier) and does not choose ### them. This feature can be used to include conditional transitions that ### depend on the `StateData'.

    • ###
  • `StateName(Attr1::term(), ..., AttrN::term(), ### S::'{@type state_data()}`) ::' ### `['{@type transition()}`]' ###

    There should be one instance of this function for each reachable state ### `{StateName,Attr1,...,AttrN}' of the finite state machine. The function ### has similar beaviour to `StateName/1', described above.

    • ###
  • `weight(From::'{@type state_name()}`, ### Target::'{@type state_name()}`, ### Call::'{@type symbolic_call()}`) -> integer()' ###

    This is an optional callback. When it is not defined (or not exported), ### transitions are chosen with equal probability. When it is defined, it ### assigns an integer weight to transitions from `From' to `Target' ### triggered by symbolic call `Call'. In this case, each transition is chosen ### with probability proportional to the weight assigned.

    • ###
  • `precondition(From::'{@type state_name()}`, ### Target::'{@type state_name()}`, ### StateData::'{@type state_data()}`, ### Call::'{@type symbolic_call()}`) -> boolean()' ###

    Similar to `proper_statem:precondition/2'. Specifies the ### precondition that should hold about `StateData' so that `Call' can be ### included in the command sequence. In case precondition doesn't hold, a ### new transition is chosen using the appropriate `StateName/1' generator. ### It is possible for more than one transitions to be triggered by the same ### symbolic call and lead to different target states. In this case, at most ### one of the target states may have a true precondition. Otherwise, PropEr ### will not be able to detect which transition was chosen and an exception ### will be raised.

    • ###
  • `postcondition(From::'{@type state_name()}`, ### Target::'{@type state_name()}`, ### StateData::'{@type state_data()}`, ### Call::'{@type symbolic_call()}`, ### Res::'{@type cmd_result()}`) -> boolean()' ###

    Similar to `proper_statem:postcondition/3'. Specifies the ### postcondition that should hold about the result `Res' of the evaluation ### of `Call'.

    • ###
  • `next_state_data(From::'{@type state_name()}`, ### Target::'{@type state_name()}`, ### StateData::'{@type state_data()}`, ### Res::'{@type cmd_result()}`, ### Call::'{@type symbolic_call()}`) ->' ### {@type state_data()} ###

    Similar to `proper_statem:next_state/3'. Specifies how the ### transition from `FromState' to `Target' triggered by `Call' affects the ### `StateData'. `Res' refers to the result of `Call' and can be either ### symbolic or dynamic.

    • ###
### ### === The property used === ### This is an example of a property that can be used to test a ### finite state machine specification: ### ### ```prop_fsm() -> ### ?FORALL(Cmds, proper_fsm:commands(?MODULE), ### begin ### {_History, _State, Result} = proper_fsm:run_commands(?MODULE, Cmds), ### cleanup(), ### Result =:= ok ### end).''' ### @end ### Copyright 2010-2016 Manolis Papadakis , ### Eirini Arvaniti ### and Kostis Sagonas ### ### This file is part of PropEr. ### ### PropEr is free software: you can redistribute it and/or modify ### it under the terms of the GNU General Public License as published by ### the Free Software Foundation, either version 3 of the License, or ### (at your option) any later version. ### ### PropEr is distributed in the hope that it will be useful, ### but WITHOUT ANY WARRANTY; without even the implied warranty of ### MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the ### GNU General Public License for more details. ### ### You should have received a copy of the GNU General Public License ### along with PropEr. If not, see . ### @copyright 2010-2016 Manolis Papadakis, Eirini Arvaniti and Kostis Sagonas ### @version {@version} ### @author Eirini Arvaniti ### @doc This module defines the `proper_fsm' behaviour, useful for testing ### systems that can be modeled as finite state machines. That is, a finite ### collection of named states and transitions between them. `{@module}' is ### closely related to {@link proper_statem} and is, in fact, implemented in ### terms of that. Testcases generated using `{@module}' will be on precisely ### the same form as testcases generated using {@link proper_statem}. The ### difference lies in the way the callback modules are specified. ### The relation between {@link proper_statem} and `{@module}' is similar ### to the one between `gen_server' and `gen_fsm' in OTP libraries. ### ### Due to name conflicts with functions automatically imported from ### {@link proper_statem}, a fully qualified call is needed in order to ### use the API functions of `{@module}'. ### ### === The states of the finite state machine === ### Following the convention used in `gen_fsm behaviour', the state is ### separated into a `StateName::'{@type state_name()} and some ### `StateData::'{@type state_data()}. `StateName' is used to denote a state ### of the finite state machine and `StateData' is any relevant information ### that has to be stored in the model state. States are fully ### represented as tuples `{StateName, StateData}'. ### ### `StateName' is usually an atom (i.e. the name of the state), but can also ### be a tuple. In the latter case, the first element of the tuple must be an ### atom specifying the name of the state, whereas the rest of the elements can ### be arbitrary terms specifying state attributes. For example, when ### implementing the fsm of an elevator which can reach N different floors, the ### `StateName' for each floor could be `{floor,K}, 1 <= K <= N'.
### `StateData' can be an arbitrary term, but is usually a record. ### ### === Transitions between states === ### A transition ({@type transition()}) is represented as a tuple ### `{TargetState, {call,M,F,A}}'. This means that performing the specified ### symbolic call at the current state of the fsm will lead to `TargetState'. ### The atom `history' can be used as `TargetState' to denote that a transition ### does not change the current state of the fsm. ### ### === The callback functions === ### The following functions must be exported from the callback module ### implementing the finite state machine: ###
    ###
  • `initial_state() ->' {@type state_name()} ###

    Specifies the initial state of the finite state machine. As with ### `proper_statem:initial_state/0', its result should be deterministic. ###

    • ###
  • `initial_state_data() ::' {@type state_data()} ###

    Specifies what the state data should initially contain. Its result ### should be deterministic

    • ###
  • `StateName(S::'{@type state_data()}`) ::' ### `['{@type transition()}`]' ###

    There should be one instance of this function for each reachable ### state `StateName' of the finite state machine. In case `StateName' is a ### tuple the function takes a different form, described just below. The ### function returns a list of possible transitions ({@type transition()}) ### from the current state. ### At command generation time, the instance of this function with the same ### name as the current state's name is called to return the list of possible ### transitions. Then, PropEr will randomly choose a transition and, ### according to that, generate the next symbolic call to be included in the ### command sequence. However, before the call is actually included, a ### precondition that might impose constraints on `StateData' is checked.
    ### Note also that PropEr detects transitions that would raise an exception ### of class `' at generation time (not earlier) and does not choose ### them. This feature can be used to include conditional transitions that ### depend on the `StateData'.

    • ###
  • `StateName(Attr1::term(), ..., AttrN::term(), ### S::'{@type state_data()}`) ::' ### `['{@type transition()}`]' ###

    There should be one instance of this function for each reachable state ### `{StateName,Attr1,...,AttrN}' of the finite state machine. The function ### has similar beaviour to `StateName/1', described above.

    • ###
  • `weight(From::'{@type state_name()}`, ### Target::'{@type state_name()}`, ### Call::'{@type symbolic_call()}`) -> integer()' ###

    This is an optional callback. When it is not defined (or not exported), ### transitions are chosen with equal probability. When it is defined, it ### assigns an integer weight to transitions from `From' to `Target' ### triggered by symbolic call `Call'. In this case, each transition is chosen ### with probability proportional to the weight assigned.

    • ###
  • `precondition(From::'{@type state_name()}`, ### Target::'{@type state_name()}`, ### StateData::'{@type state_data()}`, ### Call::'{@type symbolic_call()}`) -> boolean()' ###

    Similar to `proper_statem:precondition/2'. Specifies the ### precondition that should hold about `StateData' so that `Call' can be ### included in the command sequence. In case precondition doesn't hold, a ### new transition is chosen using the appropriate `StateName/1' generator. ### It is possible for more than one transitions to be triggered by the same ### symbolic call and lead to different target states. In this case, at most ### one of the target states may have a true precondition. Otherwise, PropEr ### will not be able to detect which transition was chosen and an exception ### will be raised.

    • ###
  • `postcondition(From::'{@type state_name()}`, ### Target::'{@type state_name()}`, ### StateData::'{@type state_data()}`, ### Call::'{@type symbolic_call()}`, ### Res::'{@type cmd_result()}`) -> boolean()' ###

    Similar to `proper_statem:postcondition/3'. Specifies the ### postcondition that should hold about the result `Res' of the evaluation ### of `Call'.

    • ###
  • `next_state_data(From::'{@type state_name()}`, ### Target::'{@type state_name()}`, ### StateData::'{@type state_data()}`, ### Res::'{@type cmd_result()}`, ### Call::'{@type symbolic_call()}`) ->' ### {@type state_data()} ###

    Similar to `proper_statem:next_state/3'. Specifies how the ### transition from `FromState' to `Target' triggered by `Call' affects the ### `StateData'. `Res' refers to the result of `Call' and can be either ### symbolic or dynamic.

    • ###
### ### === The property used === ### This is an example of a property that can be used to test a ### finite state machine specification: ### ### ```prop_fsm() -> ### ?FORALL(Cmds, proper_fsm:commands(?MODULE), ### begin ### {_History, _State, Result} = proper_fsm:run_commands(?MODULE, Cmds), ### cleanup(), ### Result =:= ok ### end).''' ### @end --=-=-=--