Use

CHIA has an interactive shell that works with these commands
  • General purpose commands. The general purpose commands include the commands which are used to switch the modality and to additional assistance commands:
    • list (list): lists all commands with no prefix;
    • help command (help command): shows the info related with the command;
    • exit: exits the CHIA framework
    • automata (aut): enters the automata mode
    • replacement (rep): enters the replacement mode
  • Automata mode commands. The automata commands can be used in the automata mode when a IBA (BA) is considered against the corresponding claim.
    • loadModel modelFilePath (lm modelFilePath): is used to load the model from an XML file. The XML file must match the IBA.xsd. It requires the parameter modelFilePath, i.e., the path of the file that contains the model to be checked.
    • displayModel (dispm): is used to display the model into the console.
    • loadProperty propertyFilePath (lp propertyFilePath): is used to load the property from an XML file. The XML file must match the BA.xsd. It requires the parameter propertyFilePath, i.e., the path of the file that contains the property
    • displayProperty (dispp): is used to display the property into the console.
    • loadLTLProperty LTLProperty (lpLTL LTLProperty): it is used to load the property from an LTL formula LTLProperty is the LTL formula that represents the property. The LTL formula can be created starting from a set of propositional symbols, i.e., true, false any lowercase string, a set of boolean operators, i.e., ! (negation), -> (implication), <-> (equivalence), ^ (and), v (or), and a set of temporal operators, [] (always) <> (eventually), U (until), R (realease) (Spin syntax : V), X (next).
    • check (ck): is used to check the model against the specified claim. Before running the model checking procedure it is necessary to load the model and the claim to be considered. The check command can be performed with the optional parameter
    • computeConstraint (cc): is used to compute the constraint corresponding to the model and the specified claim..
    • saveConstraint constraintFilePath (sc constraintFilePath): is used to save the constraint in an XML file. The parameter constraintFilePath is the path of the file where the constraint must be saved
    • displayConstraint (dispc): is used to display the constraint into the console.
  • Replacement mode commands. The automata commands can be used in the replacement mode when a Replacement (BA) is considered against the constraint or a specific sub-property.
    • loadConstraint constraintFilePath (lc constraintFilePath): is used to load the constraint from an XML file. The XML file must match the Constraint.xsd. It requires the parameter constraintFilePath, i.e., the path of the file that contains the constraint to be considered;
    • displayConstraint (dispc): is used to display the constraint into the console;
    • loadReplacement replacementFilePath (lr replacementFilePath): is used to load the replacement from an XML file. The XML file must mach the Replacement.xsd. The parameter replacementFilePath is the path of the file that contains the replacement to be considered;
    • displayReplacement (dispr): is used to display the replacement into the console.
    • check (ck): is used to check the replacement against the corresponding sub-property.