…In some cases it is possible to make a nondeterministic net deterministic in order to make it better suited for state space analysis. Some examples are shown below. Removing random…
Temporal logic for state spaces
…(e.g., the occurrence of certain transitions). Strongly connected components are used to make the model checking more efficient. Manual A manual describing how to use the temporal logic facilities is…
License for CPN Tools GUI
…a copy of the GNU General Public License along with CPN Tools; if not, write to the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301, USA….
License for Access/CPN
…copy of the GNU Lesser General Public License along with this library; if not, write to the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA…
License for Grade/CPN
…received a copy of the GNU General Public License along with Grade/CPN; if not, write to the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301, USA….
Data collector functions
…observation function returns integer values, the values are converted to infinite integers, i.e. IntInf.int, in order to avoid Overflow exceptions. This means that several of the functions mentioned above, such…
Add/edit inscriptions
…order of the inscriptions when using the Tab key is for places: name, type/color set, and initial marking. For transitions, the order is name, guard, time delay, and code segments….
Errors in net structure
…ML names must be unique in order to use the state space tool. Elements with non-unique ML names For more information about ML names, see the naming policy. Related pages…
Naming policy
…CP-net. State Space Tool The following criteria must be met in order to enter the state space tool: All pages must have unique ML names All places on a page…
Queues and stacks
It is often nice to be able to simulate a queue or stack discipline for places, e.g. for communication over a TCP channel. Alas, CPN Tools does not currently support…
