CircusUtils (CZT Corejava Circus 1.6-SNAPSHOT API)

java.lang.Object
- net.sourceforge.czt.circus.util.CircusUtils

public final class CircusUtils
extends Object

Author:: leo

Field Summary

Fields
Modifier and Type	Field and Description
`static CircusConcreteSyntaxSymbolVisitor`	`CIRCUS_CONCRETE_SYNTAXSYMBOL_VISITOR` Concrete syntax symbol visitor that can be used everywhere.
`static RefExpr`	`CIRCUS_ID_EXPR`
`static PowerType`	`CIRCUS_ID_TYPE` Power type of the given type for synchronisation type names.
`static ZName`	`CIRCUS_ID_TYPE_NAME` Name for name and channel set maximal types (i.e., \power~$$CIRCUSID) - the ZName ID is added by type checker to this instance
`static String`	`CIRCUS_PRELUDE` The name of the Circus prelude.
`static String`	`CIRCUS_TOOLKIT` The name of the basic Circus toolkit.
`static String`	`DEFAULT_IMPLICIT_ACTION_NAME_PREFIX`
`static String`	`DEFAULT_IMPLICIT_CHANSET_NAME_PREFIX`
`static String`	`DEFAULT_IMPLICIT_DOTEXPR_NAME_PREFIX`
`static String`	`DEFAULT_IMPLICIT_NAMESET_NAME_PREFIX`
`static String`	`DEFAULT_IMPLICIT_PROCESS_NAME_PREFIX`
`static String`	`DEFAULT_MAIN_ACTION_NAME` Every basic process main action is named with this internal name.
`static BigInteger`	`DEFAULT_MULTISYNCH` Default number of multisynchronisation occurrences for particular communication pattern.
`static ParamQualifier`	`DEFAULT_PARAMETER_QUALIFIER` Default parameter qualifier for process and actions is by value.
`static String`	`DEFAULT_PROCESS_STATE_NAME` Default name of state for stateless processes.
`static Model`	`DEFAULT_REFINEMENT_MODEL` Default model for RefinementConjPara is failures-divergences.
`static Factory`	`FACTORY`
`static RefExpr`	`SYNCH_CHANNEL_EXPR` Reference expression of the given type for synchronisation names.
`static PowerType`	`SYNCH_CHANNEL_TYPE` Power type of the given type for synchronisation type names.
`static ZName`	`SYNCH_CHANNEL_TYPE_NAME` Name for synchronisation channel type (ID is added by type checker to this instance
`static RefExpr`	`TRANSFORMER_EXPR`
`static PowerType`	`TRANSFORMER_TYPE`
`static ZName`	`TRANSFORMER_TYPE_NAME`

Method Summary

All Methods Static Methods Concrete Methods
Modifier and Type	Method and Description
`static void`	`addProofObligationAnn(Term term, Pred pred)`
`static ActionTransformerPred`	`assertActionTransformerPred(Term term)`
`static CircusChannelSetList`	`assertCircusChannelSetList(Term term)`
`static CircusCommunicationList`	`assertCircusCommunicationList(Term term)`
`static CircusFactoryImpl`	`assertCircusFactoryImpl(Object factory)`
`static CircusFieldList`	`assertCircusFieldList(Term term)`
`static CircusNameSetList`	`assertCircusNameSetList(Term term)`
`static ProcessTransformerPred`	`assertProcessTransformerPred(Term term)`
`static String`	`createAnonymousName()`
`static ZName`	`createAnonymousZName()`
`static String`	`createFullQualifiedName(String name)`
`static String`	`createFullQualifiedName(String name, int idSeed)`
`static String`	`createFullQualifiedName(String name, LocAnn loc)`
`static String`	`createFullQualifiedName(String name, LocAnn loc, boolean usePhysicalLoc)`
`static ZName`	`createFullQualifiedName(ZName name)` Calls createFullQualifiedName with the name and false for usePhysicalLoc
`static ZName`	`createFullQualifiedName(ZName name, boolean usePhysicalLoc)` Creates a fully qualified name according to the location annotation information, if avaiable.
`static BasicProcess`	`getBasicProcess(Term term)`
`static Name`	`getSchemaName(Para para)` If the given paragraph `isSimpleSchema(para)`, returns the declared schema name.
`static Map<ZName,CircusProcess>`	`getZSectImplicitProcessPara(ZSect term)` From a given ZSect term, this method extract all the implicitly declared CircusProcess definitions, which are associated with the corresponding names in the map.
`static ZParaList`	`getZSectImplicitProcessParaList(String sectName, ZParaList term)`
`static boolean`	`isActionParaSchemaValid(ActionPara ap)` Returns true if the `ActionPara` is indeed a schema expression action with a non-null `Name`.
`static boolean`	`isBasicProcess(Term term)`
`static boolean`	`isBooleanType(Object obj)`
`static boolean`	`isChannelFrom(Term term)`
`static boolean`	`isCircusGlobalPara(Para term)`
`static boolean`	`isCircusInnerProcessPara(Para term)`
`static boolean`	`isOnTheFly(Term term)`
`static boolean`	`isOutputField(Term term)`
`static boolean`	`isSimpleSchema(Para para)` Checks whether the given `Para` term is a schema or not.
`static boolean`	`isStatePara(Term term)`
`static ZName`	`qualifyName(ZName first, ZName second)`
`static CommPattern`	`retrieveCommPattern(List<Field> fields)` Returns the communication type based on the pattern of the given list of communication fields.

Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

- Field Detail
  - FACTORY
```
public static final Factory FACTORY
```
  - CIRCUS_TOOLKIT
```
public static final String CIRCUS_TOOLKIT
```
    The name of the basic Circus toolkit.
  - CIRCUS_PRELUDE
```
public static final String CIRCUS_PRELUDE
```
    The name of the Circus prelude.
  - DEFAULT_MAIN_ACTION_NAME
```
public static final String DEFAULT_MAIN_ACTION_NAME
```
    Every basic process main action is named with this internal name. Internal names start with a double dollar sign. The typechecker must guaranttee that no such names are mentioned by the user.
    
    See Also:
    
    Constant Field Values
  - DEFAULT_PROCESS_STATE_NAME
```
public static final String DEFAULT_PROCESS_STATE_NAME
```
    Default name of state for stateless processes.
    
    See Also:
    
    Constant Field Values
  - DEFAULT_IMPLICIT_ACTION_NAME_PREFIX
```
public static final String DEFAULT_IMPLICIT_ACTION_NAME_PREFIX
```
    See Also:
    
    Constant Field Values
  - DEFAULT_IMPLICIT_PROCESS_NAME_PREFIX
```
public static final String DEFAULT_IMPLICIT_PROCESS_NAME_PREFIX
```
    See Also:
    
    Constant Field Values
  - DEFAULT_IMPLICIT_DOTEXPR_NAME_PREFIX
```
public static final String DEFAULT_IMPLICIT_DOTEXPR_NAME_PREFIX
```
    See Also:
    
    Constant Field Values
  - DEFAULT_IMPLICIT_NAMESET_NAME_PREFIX
```
public static final String DEFAULT_IMPLICIT_NAMESET_NAME_PREFIX
```
    See Also:
    
    Constant Field Values
  - DEFAULT_IMPLICIT_CHANSET_NAME_PREFIX
```
public static final String DEFAULT_IMPLICIT_CHANSET_NAME_PREFIX
```
    See Also:
    
    Constant Field Values
  - DEFAULT_MULTISYNCH
```
public static final BigInteger DEFAULT_MULTISYNCH
```
    Default number of multisynchronisation occurrences for particular communication pattern. At the moment this feature is still experimental, and may disapear in the future.
  - DEFAULT_REFINEMENT_MODEL
```
public static final Model DEFAULT_REFINEMENT_MODEL
```
    Default model for RefinementConjPara is failures-divergences.
  - DEFAULT_PARAMETER_QUALIFIER
```
public static final ParamQualifier DEFAULT_PARAMETER_QUALIFIER
```
    Default parameter qualifier for process and actions is by value.
  - SYNCH_CHANNEL_TYPE_NAME
```
public static final ZName SYNCH_CHANNEL_TYPE_NAME
```
    Name for synchronisation channel type (ID is added by type checker to this instance
  - SYNCH_CHANNEL_TYPE
```
public static final PowerType SYNCH_CHANNEL_TYPE
```
    Power type of the given type for synchronisation type names. ID is added to the synch name of this instance
  - TRANSFORMER_TYPE_NAME
```
public static final ZName TRANSFORMER_TYPE_NAME
```
  - TRANSFORMER_TYPE
```
public static final PowerType TRANSFORMER_TYPE
```
  - CIRCUS_ID_TYPE_NAME
```
public static final ZName CIRCUS_ID_TYPE_NAME
```
    Name for name and channel set maximal types (i.e., \power~$$CIRCUSID) - the ZName ID is added by type checker to this instance
  - CIRCUS_ID_TYPE
```
public static final PowerType CIRCUS_ID_TYPE
```
    Power type of the given type for synchronisation type names. ID is added to the synch name of this instance
  - SYNCH_CHANNEL_EXPR
```
public static final RefExpr SYNCH_CHANNEL_EXPR
```
    Reference expression of the given type for synchronisation names. An ID is added to the synch name of this instance. This expression is not typed, even after the typechecker is created. If one creates synchronisation channels on-the-fly, one MUST type check it before use in order to add the proper powertype to the synch_channeel_expr used.
  - CIRCUS_ID_EXPR
```
public static final RefExpr CIRCUS_ID_EXPR
```
  - TRANSFORMER_EXPR
```
public static final RefExpr TRANSFORMER_EXPR
```
  - CIRCUS_CONCRETE_SYNTAXSYMBOL_VISITOR
```
public static final CircusConcreteSyntaxSymbolVisitor CIRCUS_CONCRETE_SYNTAXSYMBOL_VISITOR
```
    Concrete syntax symbol visitor that can be used everywhere.
- Method Detail
  - isActionParaSchemaValid
```
public static boolean isActionParaSchemaValid(ActionPara ap)
```
    Returns true if the ActionPara is indeed a schema expression action with a non-null Name.
  - isOutputField
```
public static boolean isOutputField(Term term)
```
  - isSimpleSchema
```
public static boolean isSimpleSchema(Para para)
```
    Checks whether the given Para term is a schema or not. That is, it checks whether either: it is an AxPara term properly encoded as either a horizontal or a boxed schema; or an ActionPara term with a SchExprAction.
  - getSchemaName
```
public static Name getSchemaName(Para para)
```
    If the given paragraph isSimpleSchema(para), returns the declared schema name. Otherwise, the method returns null.
  - isChannelFrom
```
public static boolean isChannelFrom(Term term)
```
  - isOnTheFly
```
public static boolean isOnTheFly(Term term)
```
  - isStatePara
```
public static boolean isStatePara(Term term)
```
  - isCircusInnerProcessPara
```
public static boolean isCircusInnerProcessPara(Para term)
```
  - isCircusGlobalPara
```
public static boolean isCircusGlobalPara(Para term)
```
  - getZSectImplicitProcessPara
```
public static Map<ZName,CircusProcess> getZSectImplicitProcessPara(ZSect term)
```
    From a given ZSect term, this method extract all the implicitly declared CircusProcess definitions, which are associated with the corresponding names in the map. If duplicated names are found, process paragraphs with CircusProcess definitions not marked as on-the-flyor, or on-the-fly processes with formal generic parameters, this method throws an UnsupportedAstClassException. These situations should never happen wihtin a well-implemented parser/typechecker.
  - getZSectImplicitProcessParaList
```
public static ZParaList getZSectImplicitProcessParaList(String sectName,
                                                        ZParaList term)
```
  - assertCircusFieldList
```
public static CircusFieldList assertCircusFieldList(Term term)
```
  - assertCircusFactoryImpl
```
public static CircusFactoryImpl assertCircusFactoryImpl(Object factory)
```
  - assertActionTransformerPred
```
public static ActionTransformerPred assertActionTransformerPred(Term term)
```
  - assertProcessTransformerPred
```
public static ProcessTransformerPred assertProcessTransformerPred(Term term)
```
  - assertCircusCommunicationList
```
public static CircusCommunicationList assertCircusCommunicationList(Term term)
```
  - assertCircusChannelSetList
```
public static CircusChannelSetList assertCircusChannelSetList(Term term)
```
  - assertCircusNameSetList
```
public static CircusNameSetList assertCircusNameSetList(Term term)
```
  - retrieveCommPattern
```
public static CommPattern retrieveCommPattern(List<Field> fields)
```
    Returns the communication type based on the pattern of the given list of communication fields.
    
    It returns:
    - CommPattern.Synch if the list of fields is empty.
    - CommPattern.Input if the list of fields is not empty and contain only instances of InputField.
    - CommPattern.Output if the list of fields is not empty and contain instances of either DotField.
    - CommPattern.Mixed if the list of fields is not empty and contain at least one InputField and either one DotField.
    - CommPattern.Mixed with a parser error if the list of fields is not empty but neither of the above patterns hold.
  - addProofObligationAnn
```
public static void addProofObligationAnn(Term term,
                                         Pred pred)
```
  - createFullQualifiedName
```
public static String createFullQualifiedName(String name,
                                             int idSeed)
```
  - createFullQualifiedName
```
public static String createFullQualifiedName(String name,
                                             LocAnn loc,
                                             boolean usePhysicalLoc)
```
  - createFullQualifiedName
```
public static String createFullQualifiedName(String name,
                                             LocAnn loc)
```
  - createFullQualifiedName
```
public static String createFullQualifiedName(String name)
```
  - createAnonymousName
```
public static String createAnonymousName()
```
  - createFullQualifiedName
```
public static ZName createFullQualifiedName(ZName name,
                                            boolean usePhysicalLoc)
```
    Creates a fully qualified name according to the location annotation information, if avaiable. It also considers the LocAnn.getLoc() value if usePhysicalLoc is true. If the name has no LocAnn (e.g., names created by a prover window), a unique number ID is given
    
    Parameters:
    
    name -
    
    usePhysicalLoc -
    
    Returns:
  - createFullQualifiedName
```
public static ZName createFullQualifiedName(ZName name)
```
    Calls createFullQualifiedName with the name and false for usePhysicalLoc
    
    Parameters:
    
    name -
    
    Returns:
  - createAnonymousZName
```
public static ZName createAnonymousZName()
```
  - qualifyName
```
public static ZName qualifyName(ZName first,
                                ZName second)
```
  - isBasicProcess
```
public static boolean isBasicProcess(Term term)
```
  - getBasicProcess
```
public static BasicProcess getBasicProcess(Term term)
```
  - isBooleanType
```
public static boolean isBooleanType(Object obj)
```

Class CircusUtils

Field Summary

Method Summary

Methods inherited from class java.lang.Object

Field Detail

FACTORY

CIRCUS_TOOLKIT

CIRCUS_PRELUDE

DEFAULT_MAIN_ACTION_NAME

DEFAULT_PROCESS_STATE_NAME

DEFAULT_IMPLICIT_ACTION_NAME_PREFIX

DEFAULT_IMPLICIT_PROCESS_NAME_PREFIX

DEFAULT_IMPLICIT_DOTEXPR_NAME_PREFIX

DEFAULT_IMPLICIT_NAMESET_NAME_PREFIX

DEFAULT_IMPLICIT_CHANSET_NAME_PREFIX

DEFAULT_MULTISYNCH

DEFAULT_REFINEMENT_MODEL

DEFAULT_PARAMETER_QUALIFIER

SYNCH_CHANNEL_TYPE_NAME

SYNCH_CHANNEL_TYPE

TRANSFORMER_TYPE_NAME

TRANSFORMER_TYPE

CIRCUS_ID_TYPE_NAME

CIRCUS_ID_TYPE

SYNCH_CHANNEL_EXPR

CIRCUS_ID_EXPR

TRANSFORMER_EXPR

CIRCUS_CONCRETE_SYNTAXSYMBOL_VISITOR

Method Detail

isActionParaSchemaValid

isOutputField

isSimpleSchema

getSchemaName

isChannelFrom

isOnTheFly

isStatePara

isCircusInnerProcessPara

isCircusGlobalPara

getZSectImplicitProcessPara

getZSectImplicitProcessParaList

assertCircusFieldList

assertCircusFactoryImpl

assertActionTransformerPred

assertProcessTransformerPred

assertCircusCommunicationList

assertCircusChannelSetList

assertCircusNameSetList

retrieveCommPattern

addProofObligationAnn

createFullQualifiedName

createFullQualifiedName

createFullQualifiedName

createFullQualifiedName

createAnonymousName

createFullQualifiedName

createFullQualifiedName

createAnonymousZName

qualifyName

isBasicProcess

getBasicProcess

isBooleanType