data structures and software dependability

• home

• contact

• members

• teaching

• research

• publications

• software

• events

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).

---

• News
• General Description
• Related Papers
• Download
  • Charlie
  • Plugins
  • Demo Plugin
• 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;

Related Papers

• [HSW15]
  M Heiner, M Schwarick and J Wegener:
  Charlie – an extensible Petri net analysis tool;
  In Proc. PETRI NETS 2015, Brussels, Springer, LNCS, volume 9115, pages 200–211, June 2015. [ url ] [ doi ] [ BibTeX ]
• [BHM11]
  MA Blätke, M Heiner, and W Marwan:
  Tutorial - Petri Nets in Systems Biology;
  Technical report, Otto von Guericke University Magdeburg, Magdeburg Centre for Systems Biology, August 2011. [ pdf ] [ BibTeX ]
• [WSH11]
  J Wegener, M Schwarick and M Heiner:
  A Plugin System for Charlie;
  In Proc. International Workshop on Concurrency, Specification, and Programming (CSP 2011), Biaystok University of Technology, ISBN: 978-83-62582-06-8, pages 531–554, September 2011. [ url ] [ pdf ] [ BibTeX ]
• [WSH11.sld]
  J Wegener, M Schwarick and M Heiner:
  A Plugin System for Charlie;
  Talk, International Workshop on Concurrency, Specification, and Programming (CSP 2011), September 2011. [ pdf ] [ BibTeX ]
• [Fran09]
  Andreas Franzke:
  Charlie 2.0 – a multi-threaded Petri net analyzer;
  Diploma thesis, BTU Cottbus, Dep. of CS, December 2009. [ pdf ] [ BibTeX ]
• [Fisc09]
  Ansgar Fischer:
  Reachability graph based analysis of time-dependent Petri nets (in German);
  Diploma thesis, BTU Cottbus, Dep. of CS, October 2009. [ BibTeX ]
• [Schw09]
  Marcel Schwarze:
  Web-based Petri net animation (in German);
  Diploma thesis, FH Lausitz, Dep. of CS, November 2009. [ BibTeX ]

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

1. type 'java -jar setup_charliev2_0.jar' and choose an installation folder
2. 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.