cvo-theory / apt Goto Github PK

Hi,

Thanks again for answering our questions about APT!
While experimenting with APT, we have seen an example for which it seems that APT synthesizes a PN that violates the equal-conflict property. We would like to understand this observation better.

Below is our input:

In text:

.name "Paper example"
.type LTS

.states
s0[initial]
s2
s3
s1
s4


.labels
t1
t2
t3
t4


.arcs
s0 t3 s2
s0 t2 s3
s0 t1 s1
s3 t1 s4
s1 t2 s4
s2 t4 s0
s4 t4 s0

We have used these options: upto-language-equivalence,plain,pure,safe,equal-conflict,minimize

And we obtained the synthesis result below:

In this Petri net, t1 and t3 have overlapping presets, but the preset of t1 is different from the one of t3, i.e., Preset(t1) = {p3}, preset(t3) = {p0,p3}, so they overlap but are not the same. It seems to violate the equal-conflict property.

Would you please help us understand this observation better? Do we miss something? Could this be an implementation bug?

This was noticed with the "persistent" property:
The current implementation examines all states in the LTS, however a LTS is persistent if that property is satisfied for its reachable part.

Since the same likely applies to other LTS properties, I am making this more generic.

I can see two possible ways around this:

• Explicitely calculate the reachable part of the LTS were needed (might be bad for performance)
• Implement a special module which prunes all non-reachable states from a LTS (likely bad for usability, because people wouldn't expect or remember to use this)

Hi,

first of all, my sincere congratulations for the development of this tool. It's complete and really easy to use. I want to use your tool to perform several analyses on PNs. I'd like to know more information about each module, but I've only found a way to do it, by writing in the shell commands like this:

java -jar apt.jar check_all_cycle_prop

However, it's an annoying way to get all the module descriptions one by one. I've been looking for the complete list of all the modules with their respective descriptions, but I haven't found it. One promising document was APT.pdf, but unfortunately it doesn't list them in the way I'd find useful (besides it is in german). Another alternative that I've explored is to look for this info into the source code files. I've found that most of this info is in the function String getLongDescription() of some classes which are (most of them) in the directory /Users/tama/Documents/git/apt/src/module/uniol/apt/analysis/, e.g. /Users/tama/Documents/git/apt/src/module/uniol/apt/analysis/trapsAndSiphons/TrapsModule.java. Although I think that I could be able to create a document automatically using the information in all these modules, I wonder whether you have already done it and I could save some time :)

I have another question, now related with output formats. I didn't found information about this. I wonder whether you are providing an alternative way to report the result of the analyses, like JSON, XML, or another easy-parsing format. For instance LoLa provides output using JSON, and it'd be very convenient to have something similar to ease the parsing of the results.

Thanks in advance, and again congrats for your great work.
Salva

Hi,

Thank you very much for developing this tool! We would like to use this tool in our research for Petri Net synthesis. We'd like to know if it is possible to produce free-choice solutions with this tool. If so, which options do we need to use? If not, would it be possible to add this option?

Thanks in advance and looking forward to your reply!

Kind regards,
Nan

Hi,
I've been comparing the invariants computed with Pipe to other tools, I find some divergence where Pipe is missing some invariants. More precisely, "test1a" is actually a very bad test, that is forgetting the fact that coefficients used could be negative.

I'm looking at models from the model checking contest, such as "Cloud-Deployment-PT-2a".
On this particular model after discarding test1a I can find with ITS-tools :

invariant :-1'p32 + p33 + p34 + p35 + p36 + p37 + p38 + p39 + p40 + p41 + p42 + p43 + p44 + p45 + p46 + p47 + p48 + p49 + p50 + p51 + p52 + p53 + p54 + p55 + p56 + -1'p57 = 0
invariant :p3 + -1'p57 = 0
invariant :p1 + -1'p57 = 0
invariant :p2 + -1'p32 = 0
invariant :p30 + -1'p32 = 0
invariant :-1'p32 + p67 + p68 = 0
invariant :p4 + -1'p32 = 0
invariant :-1'p32 + p58 + p59 + p60 + p61 + p62 + p65 + p66 = 0
invariant :p5 + p6 + p7 + p8 + p9 + p10 + p11 + p12 + p13 + p14 + p15 + p16 + p17 + p18 + p19 + p20 + p21 + p22 + p23 + p24 + p25 + p26 + p27 + p28 + -1'p32 + -1'p57 = 0
invariant :p29 + -1'p57 = 0
invariant :p63 + p64 + -1'p65 + -1'p66 = 0
invariant :p31 + -1'p57 = 0

Test1a discards and empties the whole matrix pretty fast.

I'm sorry my code base has diverged significantly since I forked from your code, so I can't easily propose a patch.

But I believe this "bug" exists in your code too (ie. your tool does not find the above invariants). It is not a critical bug in the sense that less invariants are reported, but the invariants are all correct. However it's a shame we miss those invariants.

This is the example model in apt format
clouDeplPT2a.tar.gz