cvo-theory / apt Goto Github PK
View Code? Open in Web Editor NEWAPT – Analysis of Petri nets and labelled transition systems
License: GNU General Public License v2.0
APT – Analysis of Petri nets and labelled transition systems
License: GNU General Public License v2.0
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.
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:
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
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.