software

C H A R L I E

latest update: March 10, 2019, at 04:22 PM

Please use the following reference to give credits to Charlie:
M Heiner, M Schwarick and J Wegener:
Charlie – an extensible Petri net analysis tool;
In Proc. PETRI NETS 2015, Brussels, Springer, LNCS, volume 9115, pp. 200–211, June 2015 (e-link).

51.7678,14.3253,ff0000: BTU Cottbus

SelectQuery error: SQLSTATE[HY000] [2002] Can't connect to local MySQL server through socket '/var/lib/mysql/mysql.sock' (2)

News
General Description
Related Papers
Download
Bug Reports
FAQ

News

June 19, 2017
- minor bug fixes
June 1, 2017
- some bug fixes
May 10, 2017
- ANDL reader supports and evaluates functions, defined in the ANDL file
- ANDL files for continuous Petri nets are supported, but any real valued number N is rounded to the smallest integer value not less than N; any additional attributes are ignored (fixed, reversible)
February 7, 2017
- some bug fixes
March 25, 2015
- new plugin for structural analysis of continuous Petri nets/ODEs is released
October 06, 2014
- some bug fixes
May 13, 2013
- some bug fixes
January 11, 2012
- import for the Abstract Net Description Language (ANDL)
December 02, 2011
- bug fix; dead transitions
August 26, 2011
- bug fix; corrected some rules
- bug fix; corrected usage of read arcs
- bug fix; list of last files can be used after Charlie restarts
- several more bug fixes
- new feature: plugin support
- new feature: option for automatically applying rules
- new feature: option for toggle on/off logging
- new feature: added reader for INA files
- new feature: improved display of results
- new feature: added several tooltips
- several more features
January 24, 2011
- bug fix; structural analysis of time nets
December 08, 2010
- bug fix; there were problems with dependent set computation
November 29, 2010
- some bug fixes; there were problems with nets containing read arcs
November 2, 2010
- the DTP computation will now be aborted when a deadlock with a not sufficiently marked trap is found; to compute all minimal deadlocks the flag 'create all' must be set
October 20, 2010
- there where problems when loading dependent node sets in snoopy; a node set file must contain an information, whether it deals with places or with transitions
- the place set analyzer has been extended: now you can determine for an arbitrary place set the maximal trap in contains
September 27, 2010
- some bug fixes, there where problems with extended arc types
Juli 22, 2010
- some bug fixes, there where problems with big sized Petri nets
January 29 , 2010
- Charlie comes with a new graphical user interface and the following additional features
- textual user interface
- marking editor
- graphical interface to use our DD-based model checkers
- analysis tasks can be done in parallel
June 3, 2009
- Charlie reads all known Petri net classes of Snoopy
- rates, timing informations etc. are irgnored; only the net structure will be considered
February 17, 2009
- bug fix concerning the determination whether a net is PURE
January 06, 2009
- the coloring of strongly connected components can be disabled
January 02, 2009
- bug fix concerning stubborn set reduction
November 27, 2008
- improvements concerning the computation of shortest paths
April 29, 2008
- bug fix in the CTL-model checker
April 8, 2008
- some bug fixes
November 23, 2007
- Charlie is now able to read P/T nets containing also read arcs, inhibitor arcs, reset arcs and equal arcs.
- Attention: The use of inhibitor arcs and reset arcs may affect analysis results (boundedness check, structural properties like DTP , ...). You should know, what you are doing!

General Description

Charlie is an extensible software tool to analyse (extended) place/transition nets, it belongs to our toolset comprising Snoopy, Marcie, Patty and S4 . The tool has been developed and is maintained at the Brandenburg Technical University (BTU), Dep. of Computer Science, "Data Structures and Software Dependability" in Cottbus, Germany. Its design builds on the experience gained over about 20 years working with INA - the Integrated Net Analyser - previously developed at Humboldt University Berlin by Peter Starke.

Charlie applies standard analysis techniques of Petri net theory to determine structural and behavioural properties of Petri nets, complemented by explicit CTL and LTL model checking.

A distinguished feature of Charlie is its rule system which applies standard theorems of Petri net theory to computed properties in order to possibly derive further properties, which may save a great amount of computational time. All applied rules are reported, so the user can keep track of the analysis process.

Charlie is a Java application, its primary focus is teaching of Petri net theory. The tool is in use for the verification of technical systems, especially software-based systems, as well as for the validation of natural systems, i.e. biochemical networks as metabolic, signal transduction, and gene regulatory networks.

Key Features

analysis of (standard) place/transition Petri nets by the standard body of Petri net theory
analysis of extended Petri nets (read/inhibitory/equal/reset arcs) based on reachability graph construction
Java application, supporting parallelism based on Java threads;
intuitive GUI
textual user interface to be embedded in external tools
rule system encoding the main theorems of the standard body of Petri net theory
extensible by plugin support

Main Analysis Features

structural analysis
- structural properties (e.g., pure, ordinary, homogenous, conservative, connected, strongly connected, boundary nodes, ...)
- net classes (state machine, marked graph, free choice, extended free choice, extended simple)
analyses building on incidence matrix
- rank theorem
- place/transition invariants
- (abstract) dependent transition sets (ADT sets)
siphon/trap computation
- Siphon/Trap Property (STP)
- place set analyser (sound/bad siphon, maximal trap)
reachability graph based analysis
- behavioural properties (boundedness, liveness, reversibility, dynamic conflicts)
- explicit CTL model checking (ctl grammar)
- explicit LTL model checking (ltl grammar)
coverability graph
path search
- shortest/longest paths between a source and sink specified by (sub-marking), state identifier or predicate
reachability/coverability graph visualization using the JUNG library

Supported Input Formats

PNML in preparation
Snoopy, all known Petri net classes, such as Petri nets, extended Petri nets, stochastic Petri nets, etc.; rates, timing informations, etc. are ignored, only the net structure is considered;

Attention: The use of special arcs (inhibitor arcs, reset arcs, etc.) may affect analysis results (boundedness check, structural properties like DTP , ...). You should know, what you are doing!
ANDL - Abstract Net Description Language, a concise, but human-readable net description language, see Marcie manual for details;
APNN - Abstract Petri Net Notation (no support of "\like", capacities);
INA's pnt format;

Downloads

Charlie

Download Charlie setup_charliev2_0.jar (19.06.2017) installation file

Requirements

Charlie is entirely implemented in Java, a Java Runtime Environment (JRE6 or higher) is required.
third party libraries
- JUNG (BSD license)
- Apache Jakarta Commons Collections 3.1 (Apache license)
- Apache Commons Logging 1.1.1 (Apache license)
- JavaHelp 2.0_05
- JCUP, JLEX (OSI license)
- ANTLR's runtime (BSD license, Copyright (c) 2003-2008, Terence Parr)

Installation/Execution

type 'java -jar setup_charliev2_0.jar' and choose an installation folder
type in this folder './run.sh' to use the graphical user interface
or './tCharlie.sh' to use the textual user interface

Plugins

Charlie comes with a plugin mechanism to extend its basic functionality. In the table below you find several plugins provided by the authors of Charlie.

Installing a plugin is simple: download the plugin file and copy the zip file (without unpacking) to the plugin folder of Charlie's installation path. ATTENTION: On MAC OS, downloading may automatically unpack the zip file. To uninstall a plugin, simply remove the file from the folder.

Name	Description	Download link
Command Line Tools	A plugin to communicate with command line tools, e.g. Marcie.	plugin-CLT.zip
Structural Reduction	A plugin trying to structurally reduce a Petri net. There are several reduction rules to choose from.	plugin-StructuralReduction.zip
Time Petri Nets	A plugin for the analysis of time-dependend Petri nets.	plugin-TimePN.zip
Conflict Graph	A plugin that computes and displays a transition conflict graph.	plugin-ConflictGraph.zip
Continuous Petri Nets	A plugin for the structural analysis of continuous Petri nets, i.e., systems of Ordinary Differential Equations (ODEs).	plugin-ODE.zip

Demo Plugin

Complete source code for Charlie's ODEs-related plugin; demonstrates how to write plugins, including the addition of new rules and properties: demo plugin charlieODE.tar.gz

Bug Reports

Submit your bug reports and comments re Charlie here.

Please check, if your problem still exists in the latest Charlie version.
Please include the information about your platform (Windows, Linux, MAC OS) and Charlie built details.

… the end …

Any comments or questions are welcome. Please direct them to monika [period] heiner [snail] b-tu [period] de Privacy Policy

data structures and software dependability

computer science department

brandenburg university of technology cottbus - senftenberg