Part of: CIF website

• Home
• Synthesis-based engineering
  • Supervisory controllers
  • Engineering approaches for supervisory controller development
    • Traditional engineering
      • Downsides of traditional engineering
    • Model-based engineering
      • Model-based engineering process
      • Benefits of model-based engineering
      • Terminology
    • Verification-based engineering
      • Verification-based engineering process
      • Benefits of verification-based engineering
    • Synthesis-based engineering
      • Synthesis-based engineering process
      • Input: plant and requirements models
      • Supervisory controller synthesis
      • Benefits of synthesis-based engineering
      • Terminology
  • Synthesis-based engineering example
    • FIFO requirement
    • Synthesis-based engineering
    • Example benefits of synthesis-based engineering
  • Synthesis-based engineering in practice
    • Development process
      • Modeling the events
      • Modeling the plant
      • Modeling plant relations
      • Modeling the requirements
      • Marking
      • Supervisor synthesis
      • Verification and validation
        • Verification
        • Validation
        • Next steps
      • Controller implementation
    • Advanced topics
      • Incremental controller development
      • Resolving issues with too limited behavior
      • Supervisor synthesis performance
      • Non-monolithic supervisor synthesis
    • Synthesis-based engineering in practice example
      • Plant specification
        • Events
        • Product identifiers
        • The INOUT place
        • The other places
      • The FIFO requirement
      • Performing synthesis
      • Simulation model
      • Simulating the supervised system
      • Manually modeled supervisor
      • Code generation
  • Challenges in applying synthesis-based engineering
    • Change in way-of-working
    • Tool support
• Language tutorial
  • Introduction
  • Lessons
  • Basics
    • Automata
    • Synchronizing events
      • Synchronization
      • Traces and state spaces
      • Concluding remarks
    • Non-determinism
      • Non-determinism between events
      • Non-determinism for single event
    • Alphabet
      • Default and implicit alphabets
      • Explicit alphabet
      • Non-default alphabet
      • Implicit vs explicit
    • Event declaration placement
    • Shorter notations
      • Self loop
      • Declaring multiple events with a single declaration
      • Multiple events on an edge
      • Nameless location
  • Data
    • Discrete variables
    • Discrete variable value changes
    • Location/variable duality (1/2)
    • Location/variable duality (2/2)
    • Global read, local write
    • Monitoring
      • The monitoring problem
      • Monitoring with self loops
      • Monitoring with monitor automata
    • Old and new values in assignments
      • Old and new values
      • Multiple assignments
      • Assignment order
      • Multi-assignments
      • Event synchronization and assignment order
    • The tau event
    • Initial values of discrete variables
    • Initialization predicates
      • Initial locations of automata
      • Consistency between initial locations and initial values
      • Restricting initialization
    • Using locations as variables
    • State (exclusion) invariants
      • Naming state (exclusion) invariants
    • State/event exclusion invariants
      • Naming state/event exclusion invariants
  • Types and values
    • Types, values, and expressions
    • Values overview
    • Integers
    • Ranged integers
    • Reals
    • Booleans
    • Strings
    • Enumerations
    • Tuples
    • Lists
    • Bounded lists and arrays
    • Sets
    • Dictionaries
    • Combining values
    • If and switch expressions
      • If expression
      • Switch expression
  • Scalable solutions and reuse (1/2)
    • Constants
    • Algebraic variables
    • Algebraic variables and equations
    • Type declarations
  • Time
    • Timing
      • Variable time
      • Timed guards
      • Time transitions
      • Urgency
      • Numeric time
    • Continuous variables
    • Continuous variables and equations
    • Equations
    • Variables overview
    • Urgency
      • Event urgency
      • Location urgency
    • Deadlock and livelock
      • Deadlock
      • Livelock
  • Channel communication
    • Channels
    • Dataless channels
    • Combining channel communication with event synchronization
  • Functions
    • Functions
    • Internal user-defined functions
    • Function statements
      • Assignment statement
      • Return statement
      • While statement
      • If statement
      • Break statement
      • Continue statement
    • Functions as values
  • Scalable solutions and reuse (2/2)
    • Automaton definition/instantiation
    • Parametrized automaton definitions
    • Automaton definition parameters
      • Algebraic parameters
      • Event parameters
        • Channel parameter usage restrictions
      • Location parameters
      • Automaton parameters
      • Multiple parameters
    • Groups
    • Group definitions
    • Imports
    • Imports and libraries
    • Imports and groups
    • Namespaces
    • Input variables
      • Hardware example
      • Co-simulation example
      • CIF models example
      • SVG image interaction example
  • Stochastics
    • Stochastics
    • Discrete, continuous, and constant distributions
      • Discrete distributions
      • Continuous distributions
      • Constant distributions
    • Pseudo-randomness
      • Pseudorandom number generator and seed
      • Simulation and initial seed
      • Sampling and tuple results
  • SVG visualization and interaction
    • SVG visualization
      • Scalable Vector Graphics (SVG)
      • CIF/SVG declarations
    • First example
      • The SVG image
      • The CIF model
      • Simulation
    • Inkscape
      • Changing ids
      • XML editor
      • Document size
      • Coordinate systems
      • Text areas
    • Sun/moon example
      • SVG image
      • CIF specification
    • Walk example
      • SVG image (walking on floor)
      • CIF specification (walking on floor)
      • SVG image (walking in room)
      • CIF specification (walking in room)
    • Rate example
      • SVG image
      • CIF specification
    • Workstation example
      • SVG image
      • CIF specification
      • Colors in SVG
    • Tank example
      • SVG image
      • CIF specification
      • Simulation
      • SVG image (revisited)
    • Lamps example
      • Introducing the lamps example
      • SVG visualization scalability issues
      • A scalable solution
    • Buffers/products example
      • SVG image
      • CIF specification
    • SVG interaction
      • Example
      • CIF/SVG input mappings
      • Single event input mapping
      • if event input mapping
      • Update input mapping
  • Text
    • Print output
      • Quick example
    • Print output examples
      • Example model and trace
      • Example 1: Printing the buffer count for all states
      • Example 2: Printing to a file
      • Example 3: Printing the odd/even status for all states
      • Example 4: Printing only for odd states
      • Example 5: Printing the result of adding an item
      • Example 6: Printing addition/removal results
      • Example 7: Printing value changes
      • Example 8: Printing headers and footers
      • Example 9: Printing the new time after time passes
      • Example 10: Printing all unique time values
      • Example 11: Printing transitions to/from a location
    • Text formatting
      • Introduction
      • Real value formatting
      • Putting values in columns
      • Large numbers
      • Left alignment
      • More formatting
  • Language extensions
    • Supervisory controller synthesis
      • Automaton kinds
      • Invariant kinds
      • Event controllability
      • Marker predicates
    • Annotations
      • Controller annotations
      • Documentation annotations
      • State annotations
• Language reference
  • Syntax
    • Lexical syntax
      • Characters
      • Keywords
      • Terminals
      • Whitespace
      • Comments
    • Grammar
    • CIF XML files
  • SVG visualization and interaction
    • CIF/SVG declarations
      • SVG file declarations
        • Paths
        • Scoping
        • Completeness and uniqueness
      • CIF/SVG copy declarations
        • Example
        • Syntax
        • Placement
        • Uniqueness
        • Overlap
        • Application
      • CIF/SVG move declarations
        • Example
        • Syntax
        • Moving graphical elements
        • Conflicting transformations
        • Application
      • CIF/SVG output mappings
        • A simple output mapping
        • Syntax
        • SVG element id
        • SVG attribute name
        • SVG presentation attributes vs CSS style attributes
        • Text labels
        • Output mapping value
        • Quoting and escaping
        • Whitespace handling
        • Uniqueness of output mappings
        • Application
      • CIF/SVG input mappings
        • Interactive elements
        • Single event input mapping
        • if event input mapping
        • Update input mapping
        • Uniqueness
  • Text
    • Print declarations
      • Transition centric view
      • Extended trace
      • Specifying the text to print
      • Quoting and escaping
      • Transition filtering
      • State filtering
      • Combining filters
      • Output file/target
      • Scoping
    • Print file declarations
      • Paths
      • Special targets
      • Scoping
      • Uniqueness
    • Text formatting details
      • Format patterns
      • Specifiers
      • Specifier syntax
      • Implicit and explicit indexing
      • Flags
      • Width
      • %b and %B specifiers
      • %d specifier
      • %x and %X specifiers
      • %e and %E specifiers
      • %f specifier
      • %g and %G specifiers
      • %s and %S specifiers
      • Escaping and quoting
      • Unused values
  • Annotations
    • Annotations
      • Syntax
      • Placement
      • Constraints
      • Naming annotations
      • Annotation providers
    • Built-in annotations
      • Controller annotations
      • Documentation annotations
      • State annotations
• Tools
  • Specification tools
    • CIF text editor
  • Supervisory controller synthesis tools
    • Data-based supervisory controller synthesis
      • Starting the data-based synthesis tool
      • Data-based synthesis options
      • Specifications supported by data-based synthesis
        • Preprocessing
        • Supported requirements
      • Early problem detection
      • Resulting supervisor
        • Namespace
        • BDD representation in CIF
      • Predicate simplification
      • Forward reachability
      • Fixed-point computations order
      • Input variables
      • Initialization
      • Performance
        • Performance-related options
      • Edge granularity
        • Linearization and non-determinism
        • Example
      • Edge order
        • Three approaches
        • Configuring the order
      • BDD variable order
        • Variable ordering options
        • Initial variable orders
        • Automatic variable ordering
          • Variable relations
          • Variable orderers
        • Advanced variable ordering configuration
          • Examples
          • Syntax
          • Orderers
          • Node finders
          • Metrics
          • Relations
          • Effects
      • BDD operation cache
      • State requirement invariants
      • Debug output
      • Statistics
      • References
    • Event-based synthesis toolset
      • Supported specifications
      • Preprocessing
      • Automaton kinds
      • Location names in reports and errors
      • Available tools
      • Event-based synchronous product
        • Starting the synchronous product tool
        • Options
      • Event-based supervisor synthesis
        • Starting the supervisor synthesis tool
        • Options
      • Event-based synthesis analysis
        • Starting the synthesis analysis tool
        • Options
      • Event-based nonconflicting check
        • Starting the nonconflicting check tool
        • Options
      • Event-based controllability check
        • Starting the controllability check tool
        • Options
      • Event-based language equivalence check
        • Starting the language equivalence check tool
        • Options
      • Event-based NFA to DFA automaton conversion
        • Starting the NFA to DFA automaton conversion tool
        • Options
      • Event-based DFA minimization
        • Starting the DFA minimization tool
        • Options
      • Event-based automaton projection
        • Starting the automaton projection tool
        • Options
      • Event-based observer check
        • Starting the observer check tool
        • Options
      • Event-based automaton abstraction
        • Starting the automaton abstraction tool
        • Options
      • Event-based trim check
        • Starting the trim check tool
        • Options
      • Event-based trim
        • Starting the trim tool
        • Options
    • CIF to Supremica transformer
      • Starting the transformation
      • Options
      • Supported specifications
      • Preprocessing
      • Transformation result
      • Initialization
      • Marking
      • State invariants
      • Alphabets
      • Range semantics
      • Jumping semantics
  • Simulation, validation, and verification tools
    • CIF simulator
      • Simulation basics
        • Supported specifications
        • Starting the simulator
        • Initialization of the CIF specification
        • Terminating the simulator
          • Initialization failure
          • Deadlock
          • Simulation end time
          • Runtime error
          • End of trace file
          • User-requested termination
            • Interactive console input
            • Interactive GUI input
            • Applications view
            • Console termination button
            • Closing last real-time visualizer
          • Confirming termination
        • Simulation of traces
          • State
          • State space
          • Traces
          • Simulation
          • Validation
        • Repeated simulation
          • Compiling just once
          • Simulating using a compiled code file
          • Option effects and priorities
          • Example
          • Applications view
      • Simulation input/output
        • Input modes
          • Interactive console input mode
            • Choosing a transition to take
            • Choosing a time transition duration
            • Choosing between termination or going back
            • Semi-automatic mode
          • Interactive GUI input mode
            • Layout
            • Availability
            • Buttons
            • Styling
            • Labels
            • Choosing an event transition
            • Choosing a time transition and duration
            • Choosing to reset the simulation
            • Choosing to undo some transitions
            • Semi-automatic mode
            • Termination
          • Automatic input mode
            • Automatic mode choice algorithm option
            • Automatic mode time transition duration option
            • Limitations
            • Undo/reset
          • Trace input mode
            • Trace file
            • Option commands
            • Transition commands
            • Simulation
          • SVG input mode
            • How it works
              • Hovering
              • Clicking
              • Queue
            • Debugging
            • Responsiveness
            • Interactive groups
          • Semi-automatic mode
          • State history
            • Enabling history
            • State stack
            • Stack size
            • Availability
            • Requests
            • Semi-automatic mode
        • Non-urgent events
          • Input modes
          • Supervisory control application domain
        • Simulation output
          • Console output
          • Normal console output
            • Available types of normal output
            • Normal output option
            • Output details
            • State filtering
            • Profiling
          • Debug console output
            • Debug output option
            • Profiling
          • Print output
            • Overwriting files
            • Single open
            • Unused print file declarations
            • Line-based output
            • Output order
            • Enabling/disabling print output
            • Undo/reset
          • SVG visualizer
            • Simulation of SVG visualizations
              • Batik rendering library
              • Unsupported SVG features
              • Unused images
              • Application order
              • SVG visualization options
              • Demonstrations
              • Undo/reset
            • Debugging SVG visualizations
              • Console debugging
              • Save as SVG
              • Stack traces
            • SVG viewer and visualizer
              • SVG viewer
              • Refresh
              • Save as
          • Trajectory data output
            • Filtering
            • Output
            • Prettifying
            • Undo/reset
          • Plot visualizer
            • Variables
            • Filtering
            • Multiple plot visualizers
            • Plot visualization modes
            • Plot visualization range
            • Data points
            • Relation to trajectory data output
            • Saving a plot image
            • Undo/reset
          • State visualizer
            • Contents
            • Icons and legend
            • Filtering
            • Multiple state visualizers
            • Undo/reset
          • Real-time simulation
            • Frames
            • Frame rate
            • Simulation speed
            • Enabling real-time simulation
            • Model time delta
            • Test mode
      • Simulation advanced topics
        • Simulator options
        • Simulation performance
          • Closing the simulator
          • Slow starting of the simulator
          • Slow termination of the simulator
          • Value simplification
          • Simulation options
        • ODE solver
          • The basics of numeric integration
            • Linear ODE
            • Nonlinear ODE
            • Discontinuities
          • The basics of numeric root finding
          • Problems with root finding
            • The problem
            • Solution 1: maximum check interval
            • Solution 2: splitting the guard
            • Debug information
          • Fixed output step size
          • Simulation end time and maximum delay
          • ODE solver integrator options
            • Integration algorithm
            • Absolute and relative tolerance
            • Minimum and maximum step size
            • Number of steps
          • ODE solver root finder options
            • Maximum check interval
            • Root finding algorithm
            • Absolute and relative tolerance
            • Maximum iterations
        • Java compiler
      • Simulation miscellaneous topics
        • Execution mode
          • Preconditions
          • Working
        • Complete mode
        • External user-defined functions
          • Termination
          • Side effects
          • Value semantics
        • External user-defined Java functions
          • External implementation reference
          • Supported types and values
          • Method resolution
          • Method invocation
          • Side effects
        • Profiling
        • Stochastic distributions and seeds
      • Simulation developer topics
        • Maximum time point tolerance
        • Debugging generated code
          • Output directory
          • Written files
          • How to use
          • Starting the simulator with generated code
        • Test mode
    • CIF to mCRL2 transformer
      • Starting the transformation
      • Options
      • Supported specifications
      • Preprocessing
      • Output of the transformation
        • Names
        • Enumerations
        • Events
        • Variable 'value' actions
        • 'marked' action
        • Behavior
        • Initialization
        • Example
    • CIF to UPPAAL transformer
      • Starting the transformation
      • Options
      • Supported specifications
      • Preprocessing
      • Transformation result
    • Controller properties checker
      • Starting the checker
      • Options
      • Supported specifications
      • Preprocessing
      • Execution scheme
      • Runtime errors
      • References
      • Bounded response check
        • Examples
        • Implementation details
      • Confluence
        • Examples
        • Implementation details
        • False negatives
      • Finite response check
        • Examples
        • Implementation details
        • False negatives
      • Non-blocking under control check
        • Examples
        • Implementation details
  • Real-time testing, code generation, and implementation tools
    • CIF code generator
      • Starting the generator
      • Options
      • Supported specifications
      • Preprocessing
      • Generated code
        • Code overview
        • Repeated execution
        • Event loops
        • Termination
        • Predictability of execution time
        • Optional execution feedback
        • Correct handling of I/O
        • Accuracy over time
        • Enumerations
        • Annotations
      • C89 code generation
        • Supported specifications
        • Differences in output
        • Options
        • Generated files
        • Compilation of the generated code
        • C89 compile-time options
        • Executing the code
        • Environment interface
        • Data access
        • Data types
        • Systematic type names
        • Runtime errors
      • C99 code generation
        • Supported specifications
        • Differences in output
        • Options
        • Generated files
        • Compilation of the generated code
        • C99 compile-time options
        • Executing the code
        • Environment interface
        • Data access
        • Data types
        • Systematic type names
        • Runtime errors
      • Java code generation
        • Supported specifications
        • Options
        • Compilation
        • Generated files
        • Executing the code
        • Environment interface
        • Data access and manipulation
        • Data types
        • Runtime errors
        • Naming
      • JavaScript code generation
        • Supported specifications
        • Options
        • Compilation
        • Generated files
        • Executing the code
        • Environment interface
        • Data access and manipulation
        • Data types
        • Runtime errors
        • Naming
      • HTML code generation
        • HTML page
          • Areas
          • Execution
          • Visualization
          • Interaction
          • Log panel
          • Settings
      • Simulink C S-Function code generation
        • Supported specifications
        • Differences in output
        • Options
        • Generated files
      • Simulink code generation and simulation example
        • System to control
        • Controller in CIF
        • Generating Simulink C code
        • Simulation in Simulink
    • CIF PLC code generator (stable)
      • Starting the generator
      • Options
        • Basic settings of the CIF PLC code generator
        • Tailoring the output of the code generator
        • Overriding target type choices
      • Supported specifications
        • Pre-processing
        • Specification checks
      • Target types
      • I/O table file
      • Continuous behavior
      • Documenting PLC code
      • Resulting PLC code
        • Names
      • TwinCAT PLC output
        • TwinCAT system modes
        • Changing modes
        • Generated output
        • Standard compliance
        • TwinCAT usage
        • Frequently Asked Questions (FAQ)
      • S7 PLC output
        • Generated output
        • Standard compliance
        • S7 usage
    • CIF PLC code generator (deprecated)
      • Starting the generator
      • Options
      • Supported specifications
      • Preprocessing
      • Standard compliance
      • Generated PLC code
      • Names
      • Program body
      • Accuracy over time
      • I/O coupling
      • PLC output type
      • TwinCAT PLC output
        • TwinCAT system modes
        • Changing modes
        • Generated output
        • TwinCAT usage
        • Frequently Asked Questions (FAQ)
      • S7 PLC output
        • Generated output
        • S7 usage
  • Miscellaneous tools
    • CIF to CIF transformer
      • Starting the transformation
      • Options
      • Transformation descriptions
      • Available transformations
      • Pretty printer
      • Add default initial values
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Anonymize names
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Convert to interface
        • Example
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Convert uncontrollable events to controllable
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Convert controllable events to uncontrollable
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Convert switch expressions to if expressions
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Eliminate algebraic variables
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Eliminate automata to string casts
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Eliminate component definition/instantiation
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Eliminate constants
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Eliminate equations
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Eliminate groups
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
          • Renaming of enumeration literals
        • Size considerations
        • Optimality
        • Annotations
      • Eliminate if updates
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Eliminate the use of locations in expressions
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Eliminate monitors
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Eliminate automaton self references
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Eliminate state/event exclusion invariants
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Eliminate tau event
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Eliminate tuple field projections
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Eliminate type declarations
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Convert enumerations to constants
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Convert enumerations to integers
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Lift events
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Linearize (merge)
        • Supported specifications
        • Preprocessing
        • Implementation details
          • Non-determinism
          • Order
          • Urgency
          • Received values and tuple field projections
          • Elimination of communication
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Linearize (product)
        • Supported specifications
        • Preprocessing
        • Implementation details
          • Non-determinism
          • Order
          • Urgency
          • Received values and tuple field projections
          • Elimination of communication
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Merge enumerations
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Default initial values
        • Switch expressions
        • Size considerations
        • Optimality
        • Annotations
      • Push print file declarations into print declarations
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Push SVG file declarations into other CIF/SVG declarations
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Relabel supervisors as plants
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Remove annotations
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Remove CIF/SVG declarations
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Remove I/O declarations
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Remove print declarations
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Remove position information
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Remove requirements
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Remove unused algebraic variables
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Remove unused events
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Simplify others
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Simplify values
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Simplify values (optimized)
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Simplify values (no references)
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
      • Simplify values (no references, optimized)
        • Supported specifications
        • Preprocessing
        • Implementation details
        • Renaming
        • Size considerations
        • Optimality
        • Annotations
    • CIF merger
      • Starting the transformation
      • Options
      • Preprocessing
      • Example
      • Shared events and variables
      • Merge compatibility
      • Merge problems
    • CIF event disabler
      • Usage scenario
      • Starting the tool
      • Supported specifications
      • Preprocessing
      • Options
      • Specifying the events to disable
      • Output
    • CIF explorer
      • Starting the program
      • Options
      • Supported specifications
      • Preprocessing
      • Output as a CIF automaton
    • CIF to yEd transformer
      • Starting the transformation
      • Options
      • Supported specifications
      • Preprocessing
      • Diagram kinds
        • Model diagram
        • Relations diagram
      • Layout
      • Structure View
  • Scripting
    • Introduction to scripting
      • Scenarios
      • Library import
      • Execution a tool
      • Command line arguments
      • Output redirection and other options
    • Overview of scriptable tools
      • Tools
      • Parameters
      • Return value
      • Implementation
• CIF examples
• CIF release notes
  • Version 6.0 (2024-12-20)
  • Version 5.0 (2024-10-03)
  • Version 4.0 (2024-06-30)
  • Version 3.0 (2024-03-31)
  • Version 2.0 (2023-12-22)
  • Version 1.0 (2023-09-30)
  • Version 0.10 (2023-06-30)
  • Version 0.9 (2023-03-31)
  • Version 0.8 (2022-12-21)
  • Version 0.7 (2022-09-30)
  • Version 0.6 (2022-07-07)
  • Version 0.5 (2022-03-29)
  • Version 0.4 (2021-12-17)
  • Version 0.3 (2021-10-01)
  • Version 0.2 (2021-07-07)
  • Version 0.1 (2021-04-02)
• Developers
  • CIF language modification
• CIF history
  • Conception
  • CIF 1
  • CIF 2
  • CIF 3
  • Eclipse ESCET
• Legal