Package jline.solvers.wrappers.jmt

Class JmtBackend

java.lang.Object

jline.solvers.wrappers.jmt.JmtBackend

public class JmtBackend
extends Object

Backend dispatch for the JMT command line. One analysis of jmt.commandline.Jmt is run on a model file and the result is left where the JMT CLI itself would leave it, that is at <model>-result.jsim for mode "sim" and <model>-result.jmva for mode "mva". Every backend satisfies that contract, so the result parsers do not know or care which one ran. Backend selection, in order:

1. options.restUrl non-empty: POST to a JMT REST server (the imperialqore/jmt-rest container). Nothing is executed locally.
2. a local JVM plus common/JMT.jar: the default, unchanged.
3. no local JVM, but Docker is usable: ask once per session whether to pull and use the JMT image, and dispatch through it.

see _kb/06-solver-catalog.md (Wrappers: three ways to reach an external binary)

Field Summary

Fields

Modifier and Type	Field	Description
static final String[]	DEFAULT_IMAGES	Docker images tried, in order, when none is named by the options.

Method Summary

Modifier and Type	Method	Description
static boolean	hasJava()	Reports whether a JVM is on the path.
static String	localCommand(String jmtPath, String mode, String modelPath, int seed)	Builds the shell command that runs one JMT analysis locally.
static String	resolveDockerImage(SolverOptions options)	Resolves the JMT Docker image to dispatch through, with user consent.
static String	resultPath(String modelPath, String mode)	Returns the path JMT writes its result to for this model and mode.
static boolean	runRemote(String mode, String modelPath, int seed, SolverOptions options)	Runs one JMT analysis through the backend the options select, when that backend is not the local JVM.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Details

DEFAULT_IMAGES

public static final String[] DEFAULT_IMAGES

Docker images tried, in order, when none is named by the options.

Method Details

resultPath

public static String resultPath(String modelPath,
 String mode)

Returns the path JMT writes its result to for this model and mode.

Parameters:

modelPath - path of the model file handed to JMT

mode - "sim" or "mva"

Returns:

the result path

hasJava

public static boolean hasJava()

Reports whether a JVM is on the path. Probed once per session: the check costs a process launch, and a JVM does not appear or vanish mid-session.

Returns:

true if "java -version" runs and exits zero

localCommand

public static String localCommand(String jmtPath,
 String mode,
 String modelPath,
 int seed)

Builds the shell command that runs one JMT analysis locally.

Parameters:

jmtPath - path of JMT.jar

mode - "sim" or "mva"

modelPath - path of the model file

seed - simulation seed, ignored by the JMVA engine

Returns:

the command line, as passed to SysUtils.system

runRemote

public static boolean runRemote(String mode,
 String modelPath,
 int seed,
 SolverOptions options)

Runs one JMT analysis through the backend the options select, when that backend is not the local JVM.

Parameters:

mode - "sim" or "mva"

modelPath - path of the model file

seed - simulation seed, ignored by the JMVA engine

options - solver options, read for restUrl and container

Returns:

true if a non-local backend ran the analysis and wrote its result file; false if the caller should run the local command

Throws:

RuntimeException - if no backend can run JMT, or a remote one failed

resolveDockerImage

public static String resolveDockerImage(SolverOptions options)

Resolves the JMT Docker image to dispatch through, with user consent. The decision is remembered for the session: a sweep over many models must not ask once per model.

Parameters:

options - solver options, read for the container override

Returns:

the image name, or null when Docker is unusable, no image can be obtained, or the user declines