Hi Chungman and Wei,
I implemented the reachability graph generation algorithms
for RT-DEVS which was invented by Dr. Tag Gon Kim.
RT-DEVS has its time advance function as an interval so
the internal schedule can be randomly selected from the interval.
I think Wei's diagnoser for a partially observe behavior needs
this RT-DEVS reachability graph.
In addition, I add "save" menu in verification engines so you
can find save functionality for saving reachability graphs.
The file name will be "RT.txt" in the folder, bin\{debug, release}.
mOOn
|