Update ModelConverter and ModelParser

.github/scripts/build.sh

@@ -1,6 +1,7 @@
 #!/bin/bash
 
 set -a
+set -x
 
 # check OS
 case $(uname) in

deps.dot

@@ -0,0 +1,125 @@
+digraph G {
+	AbstractModel -> LinearConstraint;
+	AbstractModel -> HyperRectangle;
+	AbstractModel -> FunctionSig;
+	AbstractModel -> DiscreteState;
+	AbstractModel -> DiscreteExpressions;
+	LinearConstraint -> Automaton;
+	LinearConstraint -> Constants;
+	HyperRectangle -> PVal;
+	FunctionSig -> DiscreteType;
+	DiscreteState -> Automaton;
+	DiscreteState -> AbstractValue;
+	DiscreteExpressions -> Automaton;
+	DiscreteExpressions -> AbstractValue;
+	Automaton -> NumConst;
+	AbstractValue -> ParsedValue;
+	AbstractModelUtilities -> AbstractModel;
+	AbstractProperty -> LinearConstraint;
+	AbstractProperty -> HyperRectangle;
+	AbstractProperty -> DiscreteExpressions;
+	PVal -> NumConst;
+	ParsedValue -> DiscreteType;
+	ParsedValue -> BinaryWord;
+	ParsedValue -> Constants;
+	AlgoAF -> AlgoGeneric;
+	Result -> StateSpace;
+	Options -> AbstractModel;
+	Options -> AbstractProperty;
+	Options -> AbstractAlgorithm;
+	AlgoGeneric -> Result;
+	AlgoGeneric -> Options;
+	AlgoGeneric -> ImitatorUtilities;
+	AlgoAG -> AlgoAGnot;
+	AlgoAGnot -> AlgoEUgen;
+	AlgoEUgen -> AlgoStateBased;
+	AlgoAccLoopSynth -> AlgoLoopSynth;
+	StateSpace -> State;
+	StateSpace -> AbstractAlgorithm;
+	AlgoLoopSynth -> AlgoStateBased;
+	AlgoBCCover -> AlgoCartoGeneric;
+	AlgoStateBased -> AlgoGeneric;
+	AlgoStateBased -> Statistics;
+	AlgoCartoGeneric -> AlgoStateBased;
+	AlgoCartoGeneric -> TilesManager;
+	AlgoBCCoverLearning -> AlgoBCCover;
+	AlgoBCRandom -> AlgoCartoGeneric;
+	AlgoBCRandomSeq -> AlgoCartoGeneric;
+	AlgoBCShuffle -> AlgoCartoGeneric;
+	TilesManager -> Result;
+	AlgoDeadlockFree -> AlgoPostStar;
+	AlgoPostStar -> AlgoStateBased;
+	AlgoEF -> AlgoEUgen;
+	AlgoEFmax -> AlgoEFopt;
+	AlgoEFopt -> AlgoStateBased;
+	AlgoEFmin -> AlgoEFopt;
+	State -> AbstractModel;
+	State -> AbstractProperty;
+	AlgoEFtminQueue -> AlgoStateBased;
+	AlgoEU -> AlgoEUgen;
+	AlgoGeneralizedAccLoopSynth -> AlgoLoopSynth;
+	ImitatorUtilities -> JsonFormatter;
+	AlgoIM -> AlgoIMK;
+	AlgoIMK -> AlgoStateBased;
+	AlgoIMcomplete -> AlgoIMK;
+	AlgoIMunion -> AlgoIMK;
+	AlgoNDFS -> AlgoStateBased;
+	AlgoNZCUB -> AlgoLoopSynth;
+	AlgoPRP -> AlgoIMK;
+	AlgoPTG -> AlgoGeneric;
+	AlgoPTGStrategyGenerator -> StateSpace;
+	Statistics -> ImitatorUtilities;
+	AlgoValid -> AlgoStateBased;
+	AlgorithmOptions -> AbstractProperty;
+	AlgorithmOptions -> AbstractAlgorithm;
+	CUBchecker -> AbstractModel;
+	ClocksElimination -> AbstractModel;
+	Constants -> NumConst;
+	DeadlockExtra -> StateSpace;
+	DiscreteExpressionConverter -> AbstractModel;
+	DiscreteExpressionConverter -> ParsingStructure;
+	ParsingStructure -> FunctionSig;
+	ParsingStructure -> Automaton;
+	ParsingStructure -> AbstractValue;
+	DiscreteExpressionEvaluator -> AbstractModel;
+	DiscreteExpressionEvaluator -> AbstractProperty;
+	ExpressionConverter -> AbstractModel;
+	ExpressionConverter -> TypedStructure;
+	TypedStructure -> ParsingStructure;
+	ExpressionReducer -> ParsingStructure;
+	Extrapolation -> AbstractModel;
+	Functions -> AbstractModel;
+	Functions -> ParsingStructure;
+	Graphics -> StateSpace;
+	Input -> Options;
+	LatexHeader -> Constants;
+	Logger -> JsonFormatter;
+	ModelConverter -> Options;
+	ModelConverter -> ParsingStructure;
+	ModelPrinter -> StateSpace;
+	OCamlUtilities -> NumConst;
+	OCamlUtilities -> CustomModules;
+	ObserverPatterns -> AbstractModel;
+	ObserverPatterns -> AbstractProperty;
+	ObserverPatterns -> ParsingStructure;
+	PTA2HyTech -> AbstractModel;
+	PTA2JPG -> AbstractModel;
+	PTA2JaniSpec -> AbstractModel;
+	PTA2TikZ -> AbstractModel;
+	PTA2Uppaal -> AbstractModel;
+	ParsingStructureGraph -> ParsingStructure;
+	ParsingStructureGraph -> CustomModules;
+	ParsingStructureMeta -> CustomModules;
+	ParsingStructureMeta -> ParsingStructureUtilities;
+	ParsingStructureUtilities -> ParsingStructure;
+	ParsingStructureUtilities -> JsonFormatter;
+	ParsingUtility -> Options;
+	PropertyConverter -> AbstractProperty;
+	PropertyConverter -> ParsingStructure;
+	ResultProcessor -> Result;
+	ResultProcessor -> Statistics;
+	TilesManagerConstraint -> TilesManager;
+	TilesManagerList -> TilesManager;
+	TypeConstraintResolver -> FunctionSig;
+	VariableInfo -> ParsingStructure;
+}

src/lib/ModelConverter.ml

@@ -2522,6 +2522,17 @@ let convert_property_option (useful_parsing_model_information : useful_parsing_m
 		converted_observer_structure_option
 
 
+(* TODO: Move these somewhere else? *)
+let instantiate_automaton templates parsed_template_call =
+    let user_name, template_called_name, args = parsed_template_call in
+    let template = List.find (fun t -> t.template_name = template_called_name) templates in
+    let actions, locs = template.template_body in
+    failwith "sorry"
+
+
+let instantiate_automata templates insts =
+    List.map (instantiate_automaton templates) insts
+
 (************************************************************)
 (************************************************************)
 (** MODEL AND PROPERTY CONVERSION *)
@@ -2551,6 +2562,9 @@ let abstract_structures_of_parsing_structures options (parsed_model : ParsingStr
 		)
 	in
 
+    let instantiated_automata = instantiate_automata parsed_model.template_definitions parsed_model.template_calls in
+    let all_automata = parsed_model.automata @ instantiated_automata in
+
 	(*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*)
 	(* Get names *)
 	(*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*)

src/lib/ModelParser.mly

@@ -442,8 +442,10 @@ template_calls:
     | template_call template_calls { $1 :: $2 }
     | { [] }
 
+/************************************************************/
+
 template_call:
-	| NAME OP_ASSIGN NAME LPAREN function_argument_fol RPAREN
+	| NAME OP_ASSIGN NAME LPAREN function_argument_fol RPAREN SEMICOLON
 	{
 		($1, $3, $5)
 	}