java.lang.Object

cruise.umple.nusmv.NuSMVCoordinator

public class NuSMVCoordinator
extends java.lang.Object

Field Summary

Fields

Modifier and Type Field Description

static java.lang.String NL

static java.lang.String TEXT_0

static java.lang.String TEXT_1

static java.lang.String TEXT_2
Constructor Summary

Constructors

Constructor Description

NuSMVCoordinator()

Method Summary

Modifier and Type	Method	Description
`java.lang.StringBuilder`	`_commentModel(java.lang.Integer numSpaces, java.lang.StringBuilder sb, UmpleModel model)`
`void`	`analyzeModel(UmpleModel model)`	work on this later for option argument - (currently being set - 0)
`java.util.Stack<State>`	`ancestorStack(State st)`	This adds expression to activate a composite start state
`void`	`appendConstraint(java.lang.StringBuilder output, ModuleElement property)`	Generates models from an Umple model for analysis purpose
`static java.lang.String`	`changeNameCase(java.lang.String str, int index)`	This changes the first caharacter of a given string.
`java.lang.String`	`commentModel(UmpleModel model)`
`java.lang.String`	`createFile(UmpleModel model, java.lang.StringBuilder sb, java.lang.String addOn, java.lang.String extension)`	the file with the input name on the specified path, and extension is created whenever this method returns a string (i.e.
`void`	`delete()`
`void`	`deleteAnalysisFiles(UmpleModel model)`	deletes all files used for analysis under consideration...
`boolean`	`deleteFile(java.lang.String modelFileName)`	the file with the input name on the specified path, and extension is deleted whenever this method returns true.
`java.lang.StringBuilder`	`generateModel(UmpleModel uModel, java.util.List<NuSMVModule> capsules, java.util.List<CTLSpecification> reachability, java.util.List<ModuleElement> properties, java.util.List<InvarConstraint> nonDeterminism, int option)`	Generates a String builder for the modeling elements
`java.util.List<NuSMVModule>`	`generateModuleForNestedStateMachine(StateMachine sm, UmpleClass uClass)`
`java.util.List<NuSMVModule>`	`generateModuleForSimpleStateMachine(StateMachine sm, UmpleClass uClass)`	This generates modules generated from a simple state machine including its main
`NuSMVModule`	`generateModuleForSubstate(StateMachine sm, StateMachine root)`	This generates a module for a substate given the state machine of the state and the root state machine
`java.lang.StringBuilder`	`generateModules(UmpleModel uModel, boolean temp, int option)`	Generates modules from an Umple model
`java.lang.StringBuilder`	`generateModules(UmpleModel uModel, int option)`	Generates modules from an Umple model
`java.util.List<StateMachine>`	`generateStateMachineList(StateMachine root)`	Created to generate the list of state machine
`java.lang.StringBuilder`	`generateSystem(java.util.List<NuSMVModule> modules)`
`java.util.Set<java.lang.String>`	`getAllEventNames(StateMachine sm)`	we exterminate uniqueness of auto-transitions
`java.util.List<Transition>`	`getAllTransitionsForOrthogonalState(State st)`	Harvesting transitions for any given orthogonal state or region
`java.util.List<State>`	`getCompositeStates(StateMachine sm)`
`java.util.List<StateMachine>`	`getEmbeddedStateMachines(State state)`	Computes the list of embeddedStateMachines of a composite state
`java.lang.String`	`getExpression(java.util.ArrayDeque<java.lang.String> nodes)`
`int`	`getObjectIdentity(StateMachine sm, java.lang.Object obj)`
`<E> boolean`	`has(java.util.Collection<E> objectList, E whatToFind)`
`boolean`	`isIgnorablePair(Transition first, Transition second, State supremum)`	This checks whether the input transitions are ignorable for non-determinism
`boolean`	`isNested(StateMachine sm)`
`boolean`	`isSourceEmbedded(Transition first, Transition second)`	Tracks non-determinism whenever one of the pairable transitions incidents on the supremum and the other incidents on an embedded state
`void`	`prepareAnalysisFiles(UmpleModel model, java.lang.StringBuilder output, ModuleElement element)`	prepares all files needed for analysis under consideration...
`void`	`printList(java.util.List<Transition> input, StateMachine root)`
`java.lang.String`	`toString()`

Methods inherited from class java.lang.Object

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

Field Details
- NL
  
  public static final java.lang.String NL
- TEXT_0
  
  public static final java.lang.String TEXT_0
  
  See Also:
  
  Constant Field Values
- TEXT_1
  
  public static final java.lang.String TEXT_1
  
  See Also:
  
  Constant Field Values
- TEXT_2
  
  public static final java.lang.String TEXT_2
Constructor Details
- NuSMVCoordinator
  
  public NuSMVCoordinator()
Method Details
- delete
  
  public void delete()
- changeNameCase
  
  public static java.lang.String changeNameCase(java.lang.String str, int index)
  
  This changes the first caharacter of a given string.
  
  Parameters:
  
  str - the given string.
  
  index - value 0 - Lowercase, 1 - Uppercase, Otherwise no change
  
  Returns:
  
  the resulting string value.
- isNested
  
  public boolean isNested(StateMachine sm)
- generateSystem
  
  public java.lang.StringBuilder generateSystem(java.util.List<NuSMVModule> modules)
- generateStateMachineList
  
  public java.util.List<StateMachine> generateStateMachineList(StateMachine root)
  
  Created to generate the list of state machine
- getEmbeddedStateMachines
  
  public java.util.List<StateMachine> getEmbeddedStateMachines(State state)
  
  Computes the list of embeddedStateMachines of a composite state
- getCompositeStates
  
  public java.util.List<State> getCompositeStates(StateMachine sm)
- generateModel
  
  public java.lang.StringBuilder generateModel(UmpleModel uModel, java.util.List<NuSMVModule> capsules, java.util.List<CTLSpecification> reachability, java.util.List<ModuleElement> properties, java.util.List<InvarConstraint> nonDeterminism, int option)
  
  Generates a String builder for the modeling elements
- createFile
  
  public java.lang.String createFile(UmpleModel model, java.lang.StringBuilder sb, java.lang.String addOn, java.lang.String extension)
  
  the file with the input name on the specified path, and extension is created whenever this method returns a string (i.e. absolute file name).
- deleteFile
  
  public boolean deleteFile(java.lang.String modelFileName)
  
  the file with the input name on the specified path, and extension is deleted whenever this method returns true.
- prepareAnalysisFiles
  
  public void prepareAnalysisFiles(UmpleModel model, java.lang.StringBuilder output, ModuleElement element)
  
  prepares all files needed for analysis under consideration...
- analyzeModel
  
  public void analyzeModel(UmpleModel model)
  
  work on this later for option argument - (currently being set - 0)
- deleteAnalysisFiles
  
  public void deleteAnalysisFiles(UmpleModel model)
  
  deletes all files used for analysis under consideration...
- appendConstraint
  
  public void appendConstraint(java.lang.StringBuilder output, ModuleElement property)
  
  Generates models from an Umple model for analysis purpose
- generateModules
  
  public java.lang.StringBuilder generateModules(UmpleModel uModel, boolean temp, int option)
  
  Generates modules from an Umple model
- generateModules
  
  public java.lang.StringBuilder generateModules(UmpleModel uModel, int option)
  
  Generates modules from an Umple model
- generateModuleForNestedStateMachine
  
  public java.util.List<NuSMVModule> generateModuleForNestedStateMachine(StateMachine sm, UmpleClass uClass)
- generateModuleForSimpleStateMachine
  
  public java.util.List<NuSMVModule> generateModuleForSimpleStateMachine(StateMachine sm, UmpleClass uClass)
  
  This generates modules generated from a simple state machine including its main
- generateModuleForSubstate
  
  public NuSMVModule generateModuleForSubstate(StateMachine sm, StateMachine root)
  
  This generates a module for a substate given the state machine of the state and the root state machine
- getObjectIdentity
  
  public int getObjectIdentity(StateMachine sm, java.lang.Object obj)
- isIgnorablePair
  
  public boolean isIgnorablePair(Transition first, Transition second, State supremum)
  
  This checks whether the input transitions are ignorable for non-determinism
- isSourceEmbedded
  
  public boolean isSourceEmbedded(Transition first, Transition second)
  
  Tracks non-determinism whenever one of the pairable transitions incidents on the supremum and the other incidents on an embedded state
- getAllTransitionsForOrthogonalState
  
  public java.util.List<Transition> getAllTransitionsForOrthogonalState(State st)
  
  Harvesting transitions for any given orthogonal state or region
- printList
  
  public void printList(java.util.List<Transition> input, StateMachine root)
- ancestorStack
  
  public java.util.Stack<State> ancestorStack(State st)
  
  This adds expression to activate a composite start state
- getAllEventNames
  
  public java.util.Set<java.lang.String> getAllEventNames(StateMachine sm)
  
  we exterminate uniqueness of auto-transitions
- getExpression
  
  public java.lang.String getExpression(java.util.ArrayDeque<java.lang.String> nodes)
- _commentModel
  
  public java.lang.StringBuilder _commentModel(java.lang.Integer numSpaces, java.lang.StringBuilder sb, UmpleModel model)
- commentModel
  
  public java.lang.String commentModel(UmpleModel model)
- toString
  
  public java.lang.String toString()
  
  Overrides:
  
  toString in class java.lang.Object
- has
  
  public <E> boolean has(java.util.Collection<E> objectList, E whatToFind)

Modifier and Type	Field	Description
`static java.lang.String`	`NL`
`static java.lang.String`	`TEXT_0`
`static java.lang.String`	`TEXT_1`
`static java.lang.String`	`TEXT_2`

Class NuSMVCoordinator

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Field Details

Constructor Details

Method Details