pierreganty / mist Goto Github PK

@pevalme can you revise the documentation of typechecking.c ? The current documentation does not explain what triggers return false.
Also the use of MAX_INT looks suspicious (why 16bits?).

better explain what's needed to build mist

make them parametric using a macro language, e.g. m4

The wiki contains a warning note which might not be valid anymore.

graphs are being displayed correctly with Safari (7.1.4) and Firefox (37.0)

From the compare below, I see that many examples do not contain their #expected result: {safe,unsafe} result. Those are all the examples renamed but with 0 lines added / deleted.

e64535f...248e7ae#diff-45d33d1bf59503720e58e2d5a82c844b

@pevalme Currently graphs in the web browser are one column.
It would be great to better use the screen real estate with the graphs displayed in table (tile layout).
What are the possible options ?

We want to add a timeout option to the command line. Mist will kill itself when it consumes more than the max time it is allowed.
What C functions to use is up to you, you can start with this link.

By examining the ist of the target, report when it is a coverability instance and when it is not.

Revisit the types generated by the Pascal-to-C translation (e.g. integer32) and update when necessary

Find the best way to check the problem instance is NOT a Petri net.

Update README.md with the new available options. Update the wiki too if needed.

See this tutorial.
The featuresrankdir=LR and rank=same are particularly relevant to ist.

./test_examples.py --all ../examples/boundedPN test.out 4 10
The file test.out already exists. It will be overwritten.
Do you want to continue anyways? [Y/N]
Y

make it accept lowercase y/n as well

The file will be overwritten
This script runs the algorithms of mist on the files in [folder], output is collected in [file] and compared
against expected outcomes. The script also outputs a summary of the results obtained.

this is confusing. it reads like a help message then nothing happens (because the tests are run in background) can you also output the actual values for the parameters? if not then get rid of this message.

The max number of subprocess to be used is [number of subprocess]

can you give the actual number?

Tests completed
Comparing results...
Test lamport OK
It was not a Petri Net so algorithms 'eec', 'tsi' and 'ic4pn' has not been executed

be more concise: Not a Petri Net, skipping eec tsi ic4pn

Test peterson OK
It was not a Petri Net so algorithms 'eec', 'tsi' and 'ic4pn' has not been executed
Test newdekker OK
It was not a Petri Net so algorithms 'eec', 'tsi' and 'ic4pn' has not been executed
Test newrtp INCOMPLETE
Match: eec, tsi, ic4pn
Unknown: backward
Timeout: 0 tests

Test read-write OK
It was not a Petri Net so algorithms 'eec', 'tsi' and 'ic4pn' has not been executed
Test kanban There is no expected value for this example
Safe: eec, tsi, ic4pn
Unknown: backward

If there are more unknown results than timeouts then some algorithm some example has crashed

This last message is very cryptic!

Between examples, tests and regressions it is not clear what the difference is.
Why not renaming tests into scripts and also renaming test_examples.py into run_benchmarks.py? In any case, we should add in all these 3 directories a README.md file explaining the purpose of it.
For regressions and examples perhaps renaming them to regression-tests and benchmarks would make more sense. Any ideas?

on my machine Darwin Macintosh-2.local 13.4.0 Darwin Kernel Version 13.4.0: Wed Mar 18 16:20:14 PDT 2015; root:xnu-2422.115.14~1/RELEASE_X86_64 x86_64

./src/mist --backward ./benchmarks/PN/fms.spec returns a Segmentation fault: 11

the complete output is

Copyright (C) 2002-2015 Pierre Ganty, 2003-2008 Laurent Van Begin, 2014-2015 Pedro Valero.
mist is free software, covered by the GNU General Public License, and you are
welcome to change it and/or distribute copies of it under certain conditions.
There is absolutely no warranty for mist. See the COPYING for details.


Parsing the problem instance.

./benchmarks/PN/fms.spec
Allocating memory for data structure.. DONE
System has  22 variables,  20 transitions and  2 actual invariants
Can't open file (null) so there won't be data for the graphics
Unsafe region is empty or lies outside the invariants or contains some initial states
The reached symbolic state space is:
Elems:       0 Nodes:     1 Arcs:     0 Layers:  0
Total time of computation (user)   ->  0.000 sec.
                          (system) ->  0.000 sec.
Segmentation fault: 11

The binomial coefficient computed in abstraction.c has overflown multiple times in the past.
A solution is to use a library specialized in the manipulation of large integer.
libzahl is one of them.

Get rid of ist.h possibly using tool support like IWYU

mist.c contains a hidden analyzer called eec_cegar. i think it needs to be exposed to the user through the command line. it also needs to be tested again. and used in the test scripts.

for the TTS to SPEC translation it is useful for the backward search to have an invariant.
(algorithm other than backward do not use invariants)

The invariant is
s0=1, ...,sN=1 where N is the index used by the translation. What is nice is that
the invariant is the same for all translations (unary, binary, Nary). Intuitively it reads as follows:
the sum 1*s0 + ... + 1*sN stays the same after firing a transition.
Initially (that is by the initial marking) this sum is equal to 1 (in the unary case), log N (in the binary case) and N (in the Nary case).

do not make any assumptions on the shape of these sets

From what I read here an elegant
solution for turning on and off debug output with modifying the source code is to use the following:

#ifdef DEBUG
#define DEBUG_PRINT(...) printf( __VA_ARGS__ )
#else
#define DEBUG_PRINT(...) do{ } while ( 0 )
#endif

you might consider renaming DEBUG_PRINT into PRINTF as I have seen in other projects.
This way you can keep all the printf's needed for debugging and turn them on by appending -DDEBUG when you compile.

I just saw mist.c also contains a VERBOSE flag which writes down the formulas that are manipulated during fixed point computations. Perhaps we want to implement a unique solution with verbosity level.
VERBOSE undefined or equals 0 sends all macros onto do{ } while ( 0 ).
VERBOSE 1 tells PRINTF to print something but IST_WRITE still maps onto do{ } while ( 0 )
VERBOSE 2 tells both PRINTF and IST_WRITE to print something. You got the idea.

Macros looks nice in the code because you immediately identify they are calls related to verbosity.
Also this way you don't have to comment / uncomment code.

When verbose is set high enough, generate one dot file per iterate of the fixpoint computation