Author: fahland
Date: Mon Jun 2 17:36:09 2008
New Revision: 71
URL: http://svn.gna.org/viewcvs/service-tech?rev=71&view=rev
Log:
Code refactored, changed parameters and soundness checking:
Soundness checking now distinguishes checking for reachability of end states,
checking for deadlocks, and checking for non-reachability of the final state
(this will deprecate...)
soundness analysis now appends "omega" places to each output pinset and
transitions that remove tokens from endNodes and stopNodes once the "omega"
place is marked
reachability of end states:
- adds live-locking transitions to each "omega" place
- generates the formula AG EF (omega1 > 1 OR ... OR omegaN > 0 ) AND (p1 = 0
AND ... AND pM = 0) with pi being internal places of the process
- corresponding task file and verification script is generated, verification
requires a LoLA with MODELECHECKING, executable file name "lola"
- command line call: uml2owfn -i <lib.xml> -a soundness -f <format> -o
checking for deadlocks
- adds live-locking transitions to each "omega" place
- generated verification script requires a LoLA with DEADLOCKS, executable file
name "lola_deadlock"
- command line call: uml2owfn -i <lib.xml> -a soundness -a deadlocks -f
<format> -o
inversed parameter "pins" to "keeppins" (unconnected pins are now removed by
default)
Both variants allow using Petri net reduction rules.
Modified:
trunk/uml2owfn_soundness2/src/block.cc
trunk/uml2owfn_soundness2/src/bom-process.cc
trunk/uml2owfn_soundness2/src/bom-process.h
trunk/uml2owfn_soundness2/src/globals.cc
trunk/uml2owfn_soundness2/src/options.cc
trunk/uml2owfn_soundness2/src/options.h
trunk/uml2owfn_soundness2/src/petrinet-output.cc
trunk/uml2owfn_soundness2/src/petrinet.cc
trunk/uml2owfn_soundness2/src/petrinet.h
trunk/uml2owfn_soundness2/src/uml2owfn.cc
_______________________________________________
Service-tech-commits mailing list
[email protected]
https://mail.gna.org/listinfo/service-tech-commits
