data structures and software dependability

• home

• contact

• members

• teaching

• research

• publications

• software

• events

Program: Charlie

Comments

There are some problems when we decouple "bad siphons only" from all other options. Especially when it can be selected with "stp". Then the algorithm might not find any bad siphon, because it can find a siphon with a trap that is not sufficiently marked and thus stops the computation before a bad siphon is found.

Additional Information

(1) decide stp

     - without protocol: just yes or no, and one witness for the no
         -> written to the log file;

     - with protocol written to log file, and to external file, if specified so:

       if stp does not hold
       then give
           all min siphons, which are not sufficiently marked;
           indicate all bad siphons
       else
           give the list of all minimal siphons and the contained max traps;
       endif;

(2) {check for, compute all} x [write to a file]

     x {siphons, trap}
     x {min, max}
     x { [marked, clean] sound, bad, proper}

 - sound siphon - a siphon, which contains a trap;
 - marked, sound siphon - a siphon, where the contained max trap is marked;
 - clean, sound siphon - a siphon, where the contained max trap is unmarked;
 - bad siphon - siphon, which does not contain a trap;
 - proper siphon/trap - siphon/trap, which is not a P-invariant;

Comments

to (1):

• remove "create all" checkbox and link the behavior to the "export" checkbox
• improve the output to the log file: if the stp does not hold, print all "counter examples" and then print all "good examples". if the stp holds, print all "good examples" only.

current behavior, if "create all" is selected but no other checkbox, then all computed siphons are printed

<< 00001 | BugList | 00003 >>