CA

java.lang.Object
- FSA.FSA
- - CA.CA

All Implemented Interfaces:

java.io.Serializable
```
public class CA
extends FSA
implements java.io.Serializable
```
Class implementing a Contract Automaton and its functionalities

Author:

Davide Basile

See Also:
Serialized Form

Constructor Summary

Constructors
Constructor and Description
`CA()` Invoke the super constructor and take in input the added new parameters of the automaton
`CA(int rank, int[] initial, int[] states, int[][] finalstates, CATransition[] tra)`

Method Summary

Methods
Modifier and Type	Method and Description
`boolean`	`agreement()`
`int[][]`	`allFinalStates()`
`int[][]`	`branchingCondition()`
`CA`	`clone()`
`protected Simulator`	`createSim()` Create an instance of the simulator for an FMA
`protected Transition`	`createTransition(int i)`
`int[][]`	`extendedBranchingCondition()`
`int[][]`	`getFinalStatesCA()`
`int[]`	`getInitialCA()`
`int`	`getRank()`
`int[]`	`getStatesCA()`
`CATransition[]`	`getTransition()`
`CATransition[]`	`liable()`
`int[]`	`mixedChoice()`
`CA`	`mpc()` compute the most permissive controller for agreement
`void`	`print()` Print in output a description of the automaton
`int`	`prodStates()`
`CA`	`proj(int i)` compute the projection on the i-th principal, or null if rank=1
`boolean`	`safe()`
`CA`	`smpc()` compute the most permissive controller for strong agreement
`boolean`	`strongAgreement()`
`CATransition[]`	`strongLiable()`
`boolean`	`strongSafe()`
`int`	`sumStates()`

Methods inherited from class FSA.FSA
getFinalStates, getInitial, getStates, load, run, setTransition, write

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

- Constructor Detail
  - CA
```
public CA()
```
    Invoke the super constructor and take in input the added new parameters of the automaton
  - CA
```
public CA(int rank,
  int[] initial,
  int[] states,
  int[][] finalstates,
  CATransition[] tra)
```
- Method Detail
  - print
```
public void print()
```
    Print in output a description of the automaton
    
    Overrides:
    
    print in class FSA
  - createSim
```
protected Simulator createSim()
```
    Create an instance of the simulator for an FMA
    
    Overrides:
    
    createSim in class FSA
    
    Returns:
    an instance of the simulator istantiated with this automaton
  - createTransition
```
protected Transition createTransition(int i)
```
    Overrides:
    
    createTransition in class FSA
    
    Parameters:
    i - the index of the transition to be showed as a message to the user
    
    Returns:
    a new Transition for this automaton
  - getFinalStatesCA
```
public int[][] getFinalStatesCA()
```
    Returns:
    the array of final states
  - getStatesCA
```
public int[] getStatesCA()
```
    Returns:
    the array of states
  - getInitialCA
```
public int[] getInitialCA()
```
    Returns:
    the array of initial states
  - getRank
```
public int getRank()
```
    Returns:
    the rank of the Contract Automaton
  - getTransition
```
public CATransition[] getTransition()
```
    Overrides:
    
    getTransition in class FSA
    
    Returns:
    the array of transitions
  - sumStates
```
public int sumStates()
```
  - prodStates
```
public int prodStates()
```
  - clone
```
public CA clone()
```
    Overrides:
    
    clone in class java.lang.Object
    
    Returns:
    a new object CA clone
  - proj
```
public CA proj(int i)
```
    compute the projection on the i-th principal, or null if rank=1
    
    Parameters:
    i - index of the CA
    
    Returns:
    the ith principal
  - smpc
```
public CA smpc()
```
    compute the most permissive controller for strong agreement
    
    Returns:
    KS
  - mpc
```
public CA mpc()
```
    compute the most permissive controller for agreement
    
    Returns:
    the most permissive controller for agreement
  - strongSafe
```
public boolean strongSafe()
```
    Returns:
    true if the CA is strongly safe
  - strongAgreement
```
public boolean strongAgreement()
```
    Returns:
    true if the CA admits strong agreement
  - safe
```
public boolean safe()
```
    Returns:
    true if the CA is safe
  - agreement
```
public boolean agreement()
```
    Returns:
    true if the CA admits agreement
  - branchingCondition
```
public int[][] branchingCondition()
```
    Returns:
    null if the branching condition holds, otherwise the initial state and label of the match transition together with the state where the transition is not present
  - extendedBranchingCondition
```
public int[][] extendedBranchingCondition()
```
    Returns:
    null if the ext. branching condition holds, otherwise the initial state and label of the transition together with the state where the transition is not present
  - mixedChoice
```
public int[] mixedChoice()
```
    Returns:
    the state if there are mixed choice, null otherwise
  - allFinalStates
```
public int[][] allFinalStates()
```
    Returns:
    all the final states of the CA
  - liable
```
public CATransition[] liable()
```
    Returns:
    the liable transitions
  - strongLiable
```
public CATransition[] strongLiable()
```
    Returns:
    the strongly liable transitions

Class CA

Constructor Summary

Method Summary

Methods inherited from class FSA.FSA

Methods inherited from class java.lang.Object

Constructor Detail

CA

CA

Method Detail

print

createSim

createTransition

getFinalStatesCA

getStatesCA

getInitialCA

getRank

getTransition

sumStates

prodStates

clone

proj

smpc

mpc

strongSafe

strongAgreement

safe

agreement

branchingCondition

extendedBranchingCondition

mixedChoice

allFinalStates

liable

strongLiable