@Deprecated public class SMVUtility extends java.lang.Object
FIXME: A new version for users to specify the integer bound without using abstraction of "LS" and "GT" should be implemented to support complicated update functions. Note that this has already been implemented in REDUtility.java since the format of RED 7.0 does not support these features.
|Constructor and Description|
|Modifier and Type||Method and Description|
This function generates the reachability/risk specification of a system by scanning through the subsystem, and extract states which have special risk or reachability labels.
Return a StringBuffer that contains the converted .smv format of the system.
This function decides if the director of the current actor is SR.
public static java.lang.String generateGraphicalSpecification(CompositeActor model, java.lang.String specType) throws IllegalActionException
model- The system model under analysis.
specType- The type of the graphical specification, it may be either "Risk" or "Reachability"
public static java.lang.StringBuffer generateSMVDescription(CompositeActor model, java.lang.String pattern, java.lang.String choice, java.lang.String span) throws IllegalActionException, NameDuplicationException
For previous implementation, no matter what token is sent through the
channel, the receiver only senses the existence of the token by the
XX_isPresent. We now support Boolean token recognition.
In order to introduce this mechanism,
for each signal XX, two boolean variables are introduced:
XX_isPresent: indicating whether the signal is present or not.
XX_value: indicating the value of the signal.
Therefore, now in the guard expression, it may be possible to have
XX_isPresent (in Ptolemy) ==>
XX_isPresent (in SMV)
XX == 0 (in Ptolemy) ==>
XX_isPresent && XX_value == 0 (in SMV)
XX == 1 (in Ptolemy) ==>
XX_isPresent && XX_value == 1 (in SMV)
If XX_isPresent is false, then the value of XX_value is not valid.
In SMV, there is no distinguishing between boolean T, F and numerical values 1, 0. So for the sender side, we only need to check if a sender sends a token whose value is not 0 or 1.
model- The system under analysis.
pattern- The temporal formula used to be attached in the .smv file.
choice- The type of the formula. It may be either a CTL or LTL formula.
span- A constant used to expand the domain of the variable.
public static boolean isValidModelForVerification(CompositeActor model)
model- Model used for testing.