//////////////////////////////////////////////////////////////////////////////
// Copyright (c) 2010, 2026 Contributors to the Eclipse Foundation
//
// See the NOTICE file(s) distributed with this work for additional
// information regarding copyright ownership.
//
// This program and the accompanying materials are made available
// under the terms of the MIT License which is available at
// https://opensource.org/licenses/MIT
//
// SPDX-License-Identifier: MIT
//////////////////////////////////////////////////////////////////////////////

include::../_part_attributes.asciidoc[]

:leveloffset: -2

[[tools-cifsim-chapter-supported]]
== Supported specifications

indexterm:[CIF simulator,supported specifications]
The CIF simulator supports a subset of CIF specifications.
The following restrictions apply:

* Time dependent <<lang-tut-data-chapter-stat-invariants,state invariants>> are not supported.
This applies only to state invariants.
<<lang-tut-data-chapter-stat-evt-excl-invariants,State/event exclusion invariants>> are supported.

Specifications with component definitions/instantiations are not natively supported by the CIF simulator.
Therefore, they are automatically eliminated by the simulator, as a preprocessing step, using the CIF to CIF transformation to <<tools-cif2cif-chapter-elim-comp-def-inst,eliminate component definition/instantiation>>.

Automata with multiple possible initial locations, input variables, and discrete variables with multiple possible initial values (including `any`) are not supported, unless additional <<tools-cifsim-chapter-init,initialization>> is provided.

Input variables are in principle simulated as having a constant value.
It's possible to change their values by having <<lang-tut-svg-chapter-interaction-svgin,SVG input mappings>> <<lang-tut-svg-chapter-interaction-update,update>> them, or by using the `input` commands in a <<tools-cifsim-input-trace-file,trace>> file.
Alternatively, input variables may first be <<tools-mergecif-shared,merged>> with other variables that provide their values.

The controllability of events is ignored by the simulator, as are marker predicates.

All automata are simulated as plants.
That is, all automaton kinds are ignored by the simulator.
However, simulating requirements as plants may lead to unexpected results.
Therefore, the simulator prints warnings to the console, whenever requirements are simulated.
It is highly recommended to first apply <<tools-eventbased-chapter-supervisorsynthesis,supervisor synthesis>> to the specification, and simulate the resulting specification using the simulator.
Alternatively, apply verification to the specification, <<tools-cif2cif-chapter-remove-reqs,remove>> the verified requirements, and simulate the resulting specification using the simulator.

Similar to requirement automata, the simulator warns about simulation of requirement invariants.

Annotations are ignored.
