2.0beta4: This release took a long time again. But I reviewed and changed such an amount of code, added many new tools and thoroughly tested many things. Furthermore, many other things not related to this tool demanded lots of time. Major changes had been to the GUI and the net simulator. The new version of PEP offers a lot of convenience enhancements. The analysis tools are better integrated into the GUI and it gets much simpler to extend PEP with new tools Especially the high-level net simulator and its stand-alone version, netsim_server, have been bug-fixed and extended. The simulator is fast again, using only reasonable amounts of memory again. Thus, you can simulate even large nets for long time again without killing your system. netsim_server is a stand-alone version of the simulator which can be used by the PEP GUI, but also by other clients (i.e. applications in need of a Petri net simulator). An example application is available as netsim_client, its source code should help for developing your own applications. The automaton editor has been bug fixed, and features automatic graph layout. Many analyis tools have been fixed, updated or newly integrated. A special treatment had been done with PEP's cygwin version, where a lot of errors went through the last releases. I hope that I have fixed at least the most severe ones. Only smv is still not working, but NuSMV is on its way. Due to the new tools available in PEP, this version needs at least version 1.2.0 of the PEP-externals available at http://parsys.informatik.uni-oldenburg.de/~pep/PEP2.0 The changes in detail: * peptool GUI: - general GUI changes: windows are raised when being invoked again. Most windows have default key bindings for closing and/or choosing default buttons (either Escape or Return). - peptool startup should be possible without changes to pep/bin/peptool now, if Tcl/Tk is installed in some default position - Added parameter parsing on startup. This allows for changing to some directory or even opening a project directly - Many tools now send their output back to Tcl directly, instead of using intermediate files. Also changed some tools to allow stdout as output stream - Removed many bitmaps used for formula buttons. Now text is used on the buttons - Fixed some formula syntax, added some new modes for new tools - Fixed project handling - Fixed wrong menu names - Changed project file format due to many renamed/replaced entries - Fixed deadlock dialog to update correctly - Fixed Spin formula and result handling, added some more options - Changed SMV file handling. The specification is added directly when model checking, thus a regeneration of smv code is not needed anymore if onyl the formula is changed. - Fixed mercutio example sequence calculation - Some more tools check for missing input files and generate them on their own - Analysis tools handling much simplified. Errors are captured easier, execution and result display is done uniformly. Now all tools display time used - Added counter example transformation for unfsmodels - Fixed open option dialog error - Fixed prod example sequence generation - Fixed lola problems and integrated single checks directly into PEP * Net editors: - The major mem leak has been fixed. Was due to double instantiation of strings, losing one reference - The analysis of guards has been reenabled, which leads to dramatic speedups in high-level net simulation. Had been disabled by some wrong parsing in between. Also fixed some problems in these routines which prevented to get full benefits from them. Also fixed some range checks which lead to wrong tokens sometimes. - Major Tcl code enhancements. Many parts for high- and low-level nets reused instead of duplicated - Node types and Annotation names are displayed in the message entry if mouse moves over an element in the canvas - High-level tokens finally displayed correctly in all cases - The simulation server received major updates. Also netsim_client has been updated to be useful for others to build their own standalone Petri net applications from it. Also fixed some problems between PEP GUI and server. Uses lots of STL algorithms now. Server commands Typ and Marking renamed to Type and CurrentMarking. This makes the other command named Marking accessible again. - Fixed AllBindings switch - Menu layout changed. Saved code and should be more intuitive - Full repaint is used less often - Statistics gathered automatically if statistics window is opened - Updated sequence handling. Sequence is reset when net is reset - Area creation should be more intuitive, now (no need for another click) - Fixed annotation jumping on selecting their nodes - Fixed time annotation handling - Fixed editor crashes on parse error - Nicer placement of annotations - Removed net format conversion from old tupel access to new scheme. This should not be used by anyone for many years, now. - Fixed some mouse event handling errors - Fixed bug when closing empty editor - Correctly update active transitions after net reset * Automata editor: - Added automatic layout using graphplace and graphviz. graphviz has to be installed manually due to its size - Added some stategraph to automata conversion routines. Tina stategraphs can be loaded and thereby automatically transformed. - Fixed problem with spaces in labels - Fixed edge creation - Fixed display of start and end vertex names * Text editors: - Added font family selector - Fixed file extension filters * CYGWin related: - Fixed strutural dialog not working due to inf upper bound for spinbox.Seems to be a problem of strtod under cygwin - Same error but really fixed in net editors for latest firing time. String is parsed by Tcl and signaled as -1 to make it working - Hopefully fixed script exec'ing under cygwin - Fixed gcc detection under cygwin - Fixed color scheme under cygwin - Fixed rpc communication - Scrollbars under cygwin were ugly, now fixed - Tried to give another workaround for the link exec problem under cygwin * Added bpn2promela, which translates bpn^2 program directly into promela code. Not yet working correctly. * Added dssz model checking tools * Changed pep2spin. Fixed bug with weights. Added terminal marking parameter, which allows to declare the terminal marking as good state. Removed DEADLOCK variable, instead use valid end states check from spin to check for deadlocks. Fixed transition file to correct example sequences. * Fixed pep2smv helper tools. gencomp did not number the places correctly. transsmv rewritten in large parts to become compatible with NuSMV, which is not yet integrated, but stable to use. Especially for cygwin users, where smv core dumps. * Fixed bpn2pbc syntax checker (also in text editor handling) * Fixed named blocks in b2b * Fixed pep2lp place numbering * Fixed pfa2bpn infinite loop * Fixed bounded statistics reporting wrong numbers of stategraph * FreeBSD compatibility and some other patches contributed by Jaap Boender * Fixed inatcl_start, which allows to use a different Tcl version for inatcl * externals are only made on request, not as part of make all * Removed the 3D Java part, was not working anyway 2.0beta3: As mentioned with the last CHANGES, beta2 was not tested very well. Due to Murphy, some versions failed to work completely. This is especially true for the cygwin release, where even startup failed due to missing tcl indices. This release will hopefully work better. Additionally, and this is why I call it Darwin release, PEP now compiles under MacOS X (aka. Darwin). Thanks to Ulrich Hobelmann, who searched the code for incompatibilities and figures out how to compile dynamc libraries under darwin, I updated the code to become at least compilable. Due to the lack of hardware I cannot test the executables, nor can I provide binaries in a tar ball (Even the SourceForge Compilefarm dows not work - Tk is missing). But you're free to compile it on your own and provide a fresh tarball to be published on the SF pages. Here are the changes since beta2: - Fixed counterexample simulation in net editors. The menu item execute transition now does the same as the play button - Cleanup in Net editor Programming Dialogs - Fixed NetDelete and many other small runtime bugs - Arc annotations can change their fonts, now. Also working for weights in LL nets - Fixed the arc dialog. Should work now as with nodes, i.e. double-1 opens dialog and motion-1 moves the arc. button-2 straightens the arc. The little helper square has been removed - Some fixes for search routine in Net editor. Added Ctrl-f shortcut for find - Rewritten graph layout script for benchmarking results using tklib - Fix for mcsmodels firing sequence calculation - Fixed some core dumps in standalone Tcl executables (usually not used from PEP) - Another fix for cygwin. Removed t option to mode field in fopen call. Does not work and is not needed - Added Fast Net Simulation without any graphical update. Not yet finished. - Many changes for MacOS X dynamic library support - One can compile the PEP code without libxml2 support. This will result in loss of PNML support and inability to load SDL models in the graphical editor - Some more pfa_edit fixes. Arcs should load correctly, now. The nodes should be selectable again, as before. - Instead of using ranlib I added the s option to ar. I hope that this will work on all systems - Replaced libxercesc by libxml2 in sdl_edit. This allows its use under cygwin, too, since the old libxerces version one had to use before did not support cygwin. There are a lot of mem leaks, however, due to the libxml2 string handling. - Fixed opening sdl text files in pep editor - Fixed TCLLIBPATH in startup script - Lots of Tcl/Tk compatibility changes - Replaced sed script changes to string scanner/parser files by official string parser routines. Should fix the cygwin pfa2XXX and bpn2XXX compiler problems. - Fixed pnml_linegen on non-Linux systems - The external directory now stores all tar files in a new directory archive/. Please move your tar files their to avoid refetching. - Some new versions for external tools 2.0beta2: This release (Daylight saving release - at least here in Germany we added the DST hour on sunday...) is not that thoroughly tested. But since a lot of things changed I decided to make a release and probably make a new one very soon again ;-) The main changes (check CVS for all): - Newly implemented algorithms for liveness and deadlocks, specially tailored to distinct Petri net classes (T-Systems and FC-Systems). Thereby enhanced the structural tests (S/T/FC/EFC systems) and output handling (New menu button). - Boundedness uses best found bound now, e.g. if you check for bound 10 on a safe net, you will get answer yes(1), on the other hand you get no(>=10) if you check for safety on a 10-bounded net. - Added siphon calculation to TRAP tool. - A new netconvert tool is included, which allows to easily convert different net file formats into each other. This replaced pep2pnml and others. - Added an inatcl_start script which may be customized to use a locally installed Tcl/Tk 8.0 version for use with inatcl. Removed shell scripts for simulator and animator, which were not used anymore. - Reorganized Tcl code for analyzers. - Added initial version of kronos files import into PFA editor. Also available as standalone converter tool. - Fixed a number of Dialog bugs. - Added (experimental) support for pfa references. - Major rewrite of PFA editor and pfatools. * Automata in project files may use relative names. * Much C code transferred to Tcl (final_vertex, undo, load/save, copy/paste, compiling). * Tcl code enhancement (using tags on canvases, layout updates, text scan) * Enhanced functions for node creation * New code option "none" to avoid syntax checking of edges * Change of highlighting interface * Some GUI changes, esp. for mouse handling - Simplifications for pep_edit code. - Fixes for deprecated Tcl/Tk functions and variables. - NetEdit updates: * Updated panning functions for NetEdit (e.g. when searching). * Some speedup by better usage of tags in canvas. * Blocks are no images anymore. * Randomized simulation in blocks. - RPC updates to become faster and more reliable - Added romeo (reachability) and tina (liveness) tools - Added mole unfolder from mckit and options for punf. - Added lola binary, which is quite different to usual lola. Please ask for sources if you want to look at them. Hopefully fixed the initialisation of lola. 2.0beta1: We are proud to present the first beta of PEP2. The program seems to be stable enough to start the beta phase right now. This is also the first release, available via CVS from SourceForge - I hope that this will enhance the frequency for new releases, too. (Otherwise the next beta will be released in 2005 ;-) The move to SourceForge also caused some delay due to CVS problems on their side, which, on the other hand, allowed me to test this version enough to declare it beta. Before, I assumed this version to be the last alpha, but I made about two weeks of testing and improving compile issues etc. Due to legal issues I split off the external tools. They have to be downloaded from the PEP homepage separately. - The Win32 port should work now (finally!). - Moved to Tcl/Tk 8.4 due to interesting new widgets and features - removed deprecated things on the way. Also changed to gcc3. - Support for modelcheckers boundsmodels, unfsmodels, qq, LoLA. +++ Net editor +++ - Fixed synchronisation and tieing (e.g. removed unnecessary forking) in HL Editor (some fixes by Cecile Bui Thanh). - Fixed major errors in guard evaluation during binding search. - Update for Simulation server things - Fixed selection bugs - Fixed info dialogs for net elements - Simulation is better randomized - New buttons for simulation and resetting the net - Fixed most grid problems - Tokens can be removed by Shift-M now (instead of n), standard keyboard shortcuts added (Ctrl-X,C,V) - Added print dialog - Mouse wheel support for panning +++ SDL +++ - New graphical SDL editor accessible from the text editor's file menu - Changed sdl compiler to SDL-2000 syntax - Support new keywords rem, comment; and asterisk states (not really working :-( - There is a new commandline flag to restrict predefined data types to some finite range (no need to use your own sorts anymore...) +++ readpep library +++ - Fixed coordinates handling in many places - MCI Unfolding file format supports on-the-fly compression with libz - The PNML format has changed, so we changed ours, too. - mci2ll can work without calculation of layout (just reading the unfolding as a net) +++ PEP text editors +++ - Using Tk file chooser - Added Undo and Redo (available since Tk 8.4) - Using modified flag from Tk instead my own file changed flag - Using SDL-2000 syntax for highlighting now - Update for references - Added toolbar and font size selector (if you want to present your program it is hard to do with the original font size ;-) +++ PEP GUI +++ - When creating a new project, one can choose from different project layouts (still not working, though) - The GUI begins to be clever;) , i.e. some missing input files are automatically generated (if possible) - The color management does not work with Tcl/Tk 8.4 anymore. I changed this to use RPC for color propagation. - The button previously used for the FC deadlock checker now opens the common deadlock window, but I did not change the button image, yet! +++ Analysis tools +++ - New converter pep2lola for LoLA file format (low-level only, yet) - There are some efforts done for benchmarking of tools (time measurement of analysis tasks) - The deadlock tools are grouped beyond a common GUI - Update for formula syntax and transformation to allow macro expansion for all types of formulae, fixed some incompatibilities with other tools - Fixed SPIN and smv output calculation and support tools. - Fixed a problem with infinity in time labels while unfolding (was not correctly handled as infinity but as a large number). - Fixed mm model checker. Did not respect parantheses. Maximal configurations of the finite prefix are (still not completely correct) calculated or read from a file (either mci or special maximal configuration file - generator for this is included). Parts of the algorithm are due to Victor Khomenko! - Also fixed maximal configuration calculation in dlcheck (if no cutoffs are in the unfolding) - Major update for references between B(PN)^2 and Nets. Removed old reference stuff completely. - Fixed local variables for pfa2bpn. - Hope to have fixed package setup for Tcl packages. It is hard to have all shared objects at hand, while not having PEP installed. - Changed to Spin 4.0.6. - General cleanup and better reuse of common files. alpha5: This is a huge update, so its description is split into parts: Bugfixes: - Fixed severe bugs in Time unfolding. Sometimes the unfolder did not stop generating conditions as some tokens were dead, but not recognized as this. I also tuned the break points for other possibilites of stopping aging conditions. - The fc2 deadlock package did not display counterexamples, as the PEP tool for conversion has never been published. I even did not find it and hacked it quick'n'dirty. But it seems to work?! - HL-Net synchronisation had a lot of bug-fixes, but is still far from being bug-free :-( - You can safely use multiple selections and gridding now with net editors. - The C code from bpn2c should now be compilable with recent compilers. - dlcheck now supports time unfoldings. - hl2ll refuses less nets again. - most net reading and writing functions are checking variables for NULL, now. - simulation of counter examples in b(pn)^2 and SDL fixed. - simulation of counterexamples is only possible, if SEQUENCE is displayed. Otherwise an error may have occured. - No more editing of Analysis results in the display window. - scrolling in pfa_edit works again. - SDL parser refused boolean keyword (typo). - simplify is working again (maybe only broken in internal releases, though.) Updates: - Renamed EVunfold to Unfold to better distinguish between this version and the one from the Model-Checking Kit. - Removed MaxConfig calculation and minimisation from Unfolder. Configs are now calculated by the modelchecker, minimisation is done by simplify. - Included new version of SMV (2.5.4.3). - Included new version of Spin (3.4.13). - The GenForm tool has been removed, as TransForm offers better service. - Many messages have been translated to English. - Frontend and Backend are made libraries. This avoid compatibility problems, and facilitates use of their functions. No shared lib, yet. - The menu of the net editors changed a little (reordered). - Some hand-made scanners have been replaced by flex versions. I hope that I did not introduce incompatibilities. - lexan replaced x_ch completely. - UI for mca_tt updated. - peptool is the only startscript now. It contains all variable settings and the startup code. - Some dialog windows have been unified (e.g. Model checkers). - Even more exec's replaced by Tcl commands. New features: - I have ported PEP to Windows, using cygwin. It will be available very soon, maybe with the first beta of PEP2.0... - I made a simple PROD interface, checking for deadlocks only, right now. - And also added mcsmodels, also for deadlock checking right now. - The source code has been checked into a cvs repository, preparing the release. - Added check scripts for many of the tools (Only with source code). - The net editors and pfa editor are now compiled as tcl packages, not as standalone binaries (aka NetWish and pfaWish). This allows the use of Tcl Stubs, so there will be versions using any Tcl/Tk from 8.0.6 up. No more bothering about the correct version. - I used this change to update the Tcl/C interface used, now pfa_edit uses mostly Tcl_Obj, while NetEdit still uses string interface. - There is support for infinity as upper time bound now. Use 'inf' for this. Almost all tools, including the net editors, should support this. - Added Time for high-level nets, including synchronisation and unfolding to low-level nets. Note: These are just Basic Time-M-nets, i.e. no variables as time bound, yet. - New tie operator for M-nets. Offers asynchronous links (buffer places) in a compositional way. This is also available in PBC. - key bindings m and n offer adding and removing markings, if over some place in the net editor. CTRL-A allows selection of the whole net. - There is a fast simulation option for the editors, may speed up the simulation a lot, depending on the nets. Only graphical optimisation! - There are new/updated reading functions and interfaces available. Most notably, PEP allows use of PNML nets. (You need libxml2 for PEP to run!). Use pep2pnml for manual conversion from/to PNML. For the unfoldings, a common readPrefix functions allows a simple integration of the different formats, like readPEP for ll-nets. There is a tool mci2ll which produces ll-nets from unfoldings. Not very usable, yet, as the layout algorithms are still missing. - Simulation of counterexamples in HL-nets added. Known bugs: - The arc properties window does not open. Workaround: Use right mouse button. - The mci2 format is still not implemented, i.e. the unfoldings are still endianess-aware. But the tools now try to recover from these problems. - SMV output does not work, calculation of components is wrong. alpha4: - adjusted path for sdl2mnet macros. Now it uses lib/sdl2mnet without the following nets/ which was already used in lib, but not in the program itself... - New version 2.01 of clp. Bug fix for terminal markings. - Some binaries in alpha3 were broken because of 'mislinking'. I changed some compiler commands which made these binaries unable to use the pep library. This is fixed and in addition I changed the compiler on the Suns from 2.7.2.3 to 2.95.3 which should give a good speedup. But now also the Sun package needs the new stdlibc++ so I include it into the LD_LIBRARY_PATH, i.e. pep/bin/ Some files had been build with wrong flags on both architectures. This has been corrected but may change the behaviour of these programs (pep2smv and pfa2mnet) in some unpredictable way. - Some examples are not working well. This is due to a very bad design choice made for the mci-unfolding format as it is endian dependent. I will change the format in one of the next releases to big endian, for now please rebuild the finite prefix. There will be a converter from one format to the other but programmers of tools using the mci format are encouraged to change to the new format! The files are backwards compatible only if built on Suns but with the new format you may build the unfolding on Suns and modelcheck under Linux, etc. alpha3: - clp now for Solaris and Linux and in a new version. - TransForm should work now correctly. I used the old version before as I had problems using the two different yacc files. - Changed EVunfold to ignore settings not yet implemented for time petri nets (Esparza/Vogler unfolding, bitarrays,...). Be aware that the settings you change in the options dialog may not be used when unfolding time petri nets! - Fixed firing sequence production from mm with time petri nets (core dumped before) - Changed default latest firing time to 0 - Added simulation compatibility for sequences with tics (time steps). It currently beeps when simulating a time step. A strange behaviour occurs if the sequence ends with a tic. This last tic changes its name to 'ti' and thus is not recognized as a tic resulting in an error message. I don't know why this is like that, but I will keep on debugging! - Added the new tkina interface to the distribution. It will work with Tcl/Tk 8.0 now, so you don't need libtcl.7.6.so and libtk.4.2.so anymore. But you have to set TCL_LIBRARY and TK_LIBRARY pointing to the directories where you have installed init.tcl resp. tk.tcl as tkina relies on this! alpha2: - simplify always complained about two high level files. Fixed (typo). - Use new version of lp_solve (3.0->3.2) - Added destructors in HLNet and HLTransition. Don't know if they are needed, but g++ 2.7.2.3 (as used for the Suns) complained about it... Maybe I'll remove them again later on. alpha1: - initial release. Completely changed from former dists.