Browse Source

Allow .dot extension to be passed to the -exportmodel switch for export of graphical model in Dot format (less verbose and more obvious than -exporttransdotstates).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11572 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 10 years ago
parent
commit
6bcdc856c4
  1. 9
      prism/src/prism/PrismCL.java

9
prism/src/prism/PrismCL.java

@ -1871,6 +1871,9 @@ public class PrismCL implements PrismModelListener
} else if (ext.equals("lab")) { } else if (ext.equals("lab")) {
exportlabels = true; exportlabels = true;
exportLabelsFilename = basename.equals("stdout") ? "stdout" : basename + ".lab"; exportLabelsFilename = basename.equals("stdout") ? "stdout" : basename + ".lab";
} else if (ext.equals("dot")) {
exporttransdotstates = true;
exportTransDotStatesFilename = basename.equals("stdout") ? "stdout" : basename + ".dot";
} }
// Unknown extension // Unknown extension
else { else {
@ -2085,6 +2088,8 @@ public class PrismCL implements PrismModelListener
exportStatesFilename = exportStatesFilename.replaceFirst("modelFileBasename", modelFileBasename); exportStatesFilename = exportStatesFilename.replaceFirst("modelFileBasename", modelFileBasename);
if (exportlabels) if (exportlabels)
exportLabelsFilename = exportLabelsFilename.replaceFirst("modelFileBasename", modelFileBasename); exportLabelsFilename = exportLabelsFilename.replaceFirst("modelFileBasename", modelFileBasename);
if (exporttransdotstates)
exportTransDotStatesFilename = exportTransDotStatesFilename.replaceFirst("modelFileBasename", modelFileBasename);
} }
} }
@ -2346,8 +2351,8 @@ public class PrismCL implements PrismModelListener
mainLog.println("Export the built model to file(s) (or to the screen if <file>=\"stdout\")."); mainLog.println("Export the built model to file(s) (or to the screen if <file>=\"stdout\").");
mainLog.println("Use a list of file extensions to indicate which files should be generated, e.g.:"); mainLog.println("Use a list of file extensions to indicate which files should be generated, e.g.:");
mainLog.println("\n -exportmodel out.tra,sta\n"); mainLog.println("\n -exportmodel out.tra,sta\n");
mainLog.println("Possible extensions are: .tra, .srew, .trew, .sta, .lab");
mainLog.println("Use extension .all to export all and .rew to export both .srew/.trew, e.g.:");
mainLog.println("Possible extensions are: .tra, .srew, .trew, .sta, .lab, .dot");
mainLog.println("Use extension .all to export all (except .dot) and .rew to export both .srew/.trew, e.g.:");
mainLog.println("\n -exportmodel out.all\n"); mainLog.println("\n -exportmodel out.all\n");
mainLog.println("Omit the file basename to use the basename of the model file, e.g.:"); mainLog.println("Omit the file basename to use the basename of the model file, e.g.:");
mainLog.println("\n -exportmodel .all\n"); mainLog.println("\n -exportmodel .all\n");

Loading…
Cancel
Save