Author: fahland
Date: Wed May 28 00:16:50 2008
New Revision: 67
URL: http://svn.gna.org/viewcvs/service-tech?rev=67&view=rev
Log:
changed generation of nets and tasks for soundness checking:
- extended PNAPI and introduced new classes to specify CTL formulas
(AEFG-fragment)
- new class can write out LoLA-.task files for CTL model checking and for state
predicate analysis
- parameter soundness generates LoLA-.task files with the new formula class,
formula is a disjunction over (stopNodeX > 0) for all stopNodes of the net
and (endNodeY > 0 AND p1 = 0 AND ... AND pZ = 0) for all endNodes of the net
and all internal places of the net (except stopNodes and endNodes)
Added:
trunk/uml2owfn_soundness2/src/petrinet-formula.cc
trunk/uml2owfn_soundness2/src/petrinet-formula.h
Modified:
trunk/uml2owfn_soundness2/src/Makefile.am
trunk/uml2owfn_soundness2/src/petrinet-output.cc
trunk/uml2owfn_soundness2/src/petrinet.cc
trunk/uml2owfn_soundness2/src/petrinet.h
trunk/uml2owfn_soundness2/src/pnapi.h
trunk/uml2owfn_soundness2/src/uml2owfn.cc
_______________________________________________
Service-tech-commits mailing list
[email protected]
https://mail.gna.org/listinfo/service-tech-commits
