Package jline.api.mc

Class Ctmc_ssg_fj

java.lang.Object

jline.api.mc.Ctmc_ssg_fj

public final class Ctmc_ssg_fj
extends Object

Reachability-based CTMC state space generation for FJ tag-augmented structs (ModelAdapter.fjtag). Explores the global state space forward from the initial state through the regular synchronizations (sn.sync) and the fork firing synchronizations (sn.fjsync). Required for fork-join models, whose fork firings break per-chain population conservation so the population-lattice enumeration of ctmc_ssg cannot be used. Mirrors matlab/src/lang/+State/reachableSpaceGenerator.m plus its fjsync exploration block. Hash values in the returned hashed state space are 0-based row indices into sn.space, consistent with Solver_ctmc.

Method Summary

Modifier and Type	Method	Description
static CtmcSsgReachabilityResult	ctmc_ssg_fj(NetworkStruct sn, SolverOptions options)

Methods inherited from class java.lang.Object

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

Method Details

ctmc_ssg_fj

public static CtmcSsgReachabilityResult ctmc_ssg_fj(NetworkStruct sn,
 SolverOptions options)