validMEModelIdentifier: ModelExchange +> bool
validMEModelIdentifier(me) ==
	-- @OnFail("%NAME: %s not valid C variable name at %#s", me.modelIdentifier, loc2str(me.location))
	( validIdentifier(me.modelIdentifier) );

validMESourceFiles: ModelExchange +> bool
validMESourceFiles(me) ==
	me.sourceFiles <> nil =>
		-- @OnFail("%NAME: ModelExchange source file names are not unique: %s",
		-- { me.sourceFiles(a)  | a, b in set inds me.sourceFiles &
		--		a <> b and me.sourceFiles(a) = me.sourceFiles(b) } )
		( card { file | file in seq me.sourceFiles } = len me.sourceFiles );

validCSModelIdentifier: CoSimulation +> bool
validCSModelIdentifier(ecs) ==
	-- @OnFail("%NAME: %s not valid C variable name at %#s",
	-- ecs.modelIdentifier, loc2str(ecs.location))
	( validIdentifier(ecs.modelIdentifier) );

validCSSourceFiles: CoSimulation +> bool
validCSSourceFiles(ecs) ==
	ecs.sourceFiles <> nil =>
		-- @OnFail("%NAME: CoSimulation source file names are not unique: %s",
		-- { ecs.sourceFiles(a)  | a, b in set inds ecs.sourceFiles &
		--		a <> b and ecs.sourceFiles(a) = ecs.sourceFiles(b) } )
		( card { file | file in seq ecs.sourceFiles } = len ecs.sourceFiles );

validUnitNames: UnitDefinitions +> bool
validUnitNames(units) ==
	-- @OnFail("%NAME: Unit names must be unique")
	( let names = [ u.name | u in seq units ] in
		len names = card elems names );

validDisplayUnitNames: Unit +> bool
validDisplayUnitNames(unit) ==
	unit.displayUnit <> nil =>
		-- @OnFail("%NAME: DisplayUnit names must be unique within %s at %#s",
		-- unit.name, loc2str(unit.location))
		( let names = [ u.name | u in seq unit.displayUnit ] in
			len names = card elems names );

validTypeDefinitionNames: [TypeDefinitions] +> bool
validTypeDefinitionNames(tdefs) ==
	tdefs <> nil =>
		-- @OnFail("%NAME: TypeDefinition names must be unique")
		( let names = [ td.name | td in seq tdefs ] in
			len names = card elems names );

validTypeMinMax: MinMaxType +> bool
validTypeMinMax(type) ==
	let mk_(kmin, kmax) = minMaxOfKind(kindOf(type)) in allOf
	([
		-- @OnFail("%NAME: max %s is not a valid value of this type", type.max)
		( type.max <> nil => type.max <= kmax and type.max >= kmin ),

		-- @OnFail("%NAME: min %s is not a valid value of this type", type.min)
		( type.min <> nil => type.min <= kmax and type.min >= kmin ),

		-- @OnFail("%NAME: max %s not >= min %s", type.max, type.min)
		( type.min <> nil and type.max <> nil => type.max >= type.min )
	]);

validTypeDisplayUnit: SimpleType +> bool
validTypeDisplayUnit(tdef) ==
	is_Real(tdef.fmi2SimpleType) =>
		-- @OnFail("%NAME: Real %s, unit must be defined for displayUnit %s",
		-- tdef.name, tdef.fmi2SimpleType.displayUnit)
		( tdef.fmi2SimpleType.displayUnit <> nil => tdef.fmi2SimpleType.unit <> nil );

validEnumerationTypeBijection: EnumerationType +> bool
validEnumerationTypeBijection(tdef) ==
	-- @OnFail("%NAME: Enumeration item items do not form a bijection at %#s",
	-- loc2str(tdef.location))
	(
		card { i.name | i in seq tdef.item } = len tdef.item
		and	card { i.value | i in seq tdef.item } = len tdef.item
	);

validLogCategories: LogCategories +> bool
validLogCategories(cats) ==
	-- @OnFail("%NAME: LogCategory names are not unique: %s",
	-- { cats(a).name | a, b in set inds cats &
	--   a <> b and cats(a).name = cats(b).name })
	( card { c.name | c in seq cats } = len cats );

validTolerance: DefaultExperiment +> bool
validTolerance(de) ==
	-- @OnFail("%NAME: tolerance must be >= 0 at %#s", loc2str(de.location))
	( de.tolerance <> nil => de.tolerance >= 0 );

validStartStopTime: DefaultExperiment +> bool
validStartStopTime(e) ==
	-- @OnFail("%NAME: stop time must be later than start time at %#s", loc2str(e.location))
	( e.startTime <> nil and e.stopTime <> nil => e.stopTime > e.startTime );

validStepSize: DefaultExperiment +> bool
validStepSize(e) ==
	-- @OnFail("%NAME: stepSize must be less than start-stop interval at %#s", loc2str(e.location))
	( e.startTime <> nil and e.stopTime <> nil and e.stepSize <> nil =>
		e.stopTime - e.startTime > e.stepSize );

validAliasNames: ModelVariables +> bool
validAliasNames(mvs) ==
	let refmap = getAliasRefMap(mvs) in
	card dom refmap < len mvs => -- Must be some aliases
	{
		let aliases = refmap(ref) in allOf
		([
			-- @OnFail("%NAME: Multiple aliases of reference %s are settable: %s", ref,
			--		{ a.name | a in set aliases & isSettable(a) })
			( card { a | a in set aliases & isSettable(a) } <= 1 ),

			-- @OnFail("%NAME: Aliases of reference %s are settable and independent: %s", ref,
			--		{ {a.name, b.name} | a, b in set aliases &
			--			a <> b and isSettable(a) and b.causality = <independent> } )
			( not exists a, b in set aliases & a <> b and isSettable(a) and b.causality = <independent> ),

			-- @OnFail("%NAME: Too many aliases of reference %s have start set", ref)
			( card { a.fmi2ScalarVariable.start | a in set aliases &
				a.variability <> <constant> and a.fmi2ScalarVariable.start <> nil } <= 1 ),

			-- @OnFail("%NAME: Constant aliases of reference %s have different start values", ref)
			( card { a.fmi2ScalarVariable.start | a in set aliases &
				a.variability = <constant> and a.fmi2ScalarVariable.start <> nil } <= 1 ),

			-- @OnFail("%NAME: Aliases of reference %s must all be constant or variable", ref)
			( card { a | a in set aliases & a.variability = <constant> } in set {0, card aliases} ),

			-- @OnFail("%NAME: Aliases of reference %s must all have same unit/baseUnits", ref)
			( card { a.fmi2ScalarVariable.unit | a in set aliases & is_Real(a.fmi2ScalarVariable) } <= 1 ),

			/*
			* In case of different variability among the set of alias variables, and if that set of aliases
			* does not contain an input or parameter, the variability should be the highest of the variables
			* in the set, e.g. continuous > discrete > tunable > fixed. If the set includes a parameter or
			* input the aliases will have the stated variability of that parameter or input.
			*/
			let vars = { a.variability | a in set aliases } in
				if exists a in set aliases & a.causality in set {<input>, <parameter>}
				then
					let a in set aliases be st a.causality in set {<input>, <parameter>} in
						-- @OnFail("%NAME: Warning: aliases of reference %s must all be %s, because of %s",
						--		ref, a.variability, a.name)
						( vars = { a.variability } ) or true
				else
					let highest in set vars be st not exists v in set vars & varValue(v) > varValue(highest) in
						-- @OnFail("%NAME: Warning: aliases of reference %s must all be %s", ref, highest)
						( vars = { highest } ) or true
		])

		| ref in set dom refmap & card refmap(ref) > 1
	} = {true};

validIndependentVariable: ModelVariables +> bool
validIndependentVariable(mvs) ==
	-- @OnFail("%NAME: Variables define more than one independent variable: %s",
	-- { mv.name | mv in seq mvs & mv.causality = <independent> })
	( card { mv | mv in seq mvs & mv.causality = <independent> } <= 1 );

validModelVariables: ModelVariables +> bool
validModelVariables(svs) == allOf
([
	-- @OnFail("%NAME: Variables define more than one independent variable: %s",
	--	{ sv.name | sv in seq svs & sv.causality = <independent> })
	( card { sv | sv in seq svs & sv.causality = <independent> } <= 1 ),

	-- @OnFail("%NAME: Variable names are not unique: %s",
	--	{ svs(a).name | a, b in set inds svs &
	--		a <> b and svs(a).name = svs(b).name } )
	( card { sv.name | sv in seq svs } = len svs ),

	[
		-- Individual tests are OnFailed in this function
		validVariableAttributes(sv) | sv in seq svs
	]
]);

validVariableAttributes: ScalarVariable +> bool
validVariableAttributes(sv) ==
	let variable	 = sv.fmi2ScalarVariable,
		eCausality   = effectiveCausality(sv.causality, kindOf(variable)),
		eVariability = effectiveVariability(sv.variability, kindOf(variable)),
		eInitial     = effectiveInitial(sv.causality, sv.variability, sv.initial, kindOf(variable))
	in
	allOf
	([
		-- @OnFail("%NAME: Variable %s causality/variability/initial/start %s/%s/%s/%s invalid at %#s",
		-- sv.name, eCausality, eVariability, eInitial, sv.fmi2ScalarVariable.start, loc2str(sv.location))
		(
			-- Table on p46 defining causality, and p48/49 defining combinations
			cases eCausality:
				<parameter> ->
					eVariability in set {<fixed>, <tunable>}
					and eInitial = <exact>,		-- (A)

				<calculatedParameter> ->
					eVariability in set {<fixed>, <tunable>}
					and eInitial in set {<approx>, <calculated>},	-- (B)

				<input> ->
					eVariability in set {<discrete>, <continuous>}
					and eInitial = nil
					and sv.fmi2ScalarVariable.start <> nil,		-- (D)

				<independent> ->
					eVariability = <continuous>
					and eInitial = nil		-- (D)
					and sv.fmi2ScalarVariable.start = nil,

				<output> ->
					cases eVariability:
						<constant> ->
							eInitial in set {<exact>},	-- (A)

						<discrete>,
						<continuous> ->
							eInitial in set { <exact>, <approx>, <calculated> }, -- (C)

						others -> false
					end,

				<local> ->
					cases eVariability:
						<constant> ->
							eInitial = <exact>,	-- (A)

						<fixed>,
						<tunable> ->
							eInitial in set { <calculated>, <approx> },	-- (B)

						<discrete>,
						<continuous> ->
							eInitial in set { <exact>, <approx>, <calculated> } -- (C)
					end
			end
		),

		-- @OnFail("%NAME: Independent variable must be Real at %#s", loc2str(sv.location))
		(
			eCausality = <independent> => is_Real(sv.fmi2ScalarVariable)
		),

		-- @OnFail("%NAME: Variable %s variability/causality %s/%s invalid at %#s",
		-- sv.name, eVariability, eCausality, loc2str(sv.location))
		(
			-- Table on p46 defining variability, and p49 defining combinations
			cases eVariability:
				<constant> ->
					eCausality in set {<output>, <local>},

				<fixed>, <tunable> ->
					eCausality in set {<parameter>, <calculatedParameter>, <local>},

				<discrete> ->
					eCausality in set {<input>, <output>, <local>},

				<continuous> ->
					eCausality in set {<input>, <output>, <local>, <independent>}
			end
		),

		-- @OnFail("%NAME: Continuous variable must be Real at %#s", loc2str(sv.location))
		(
			eVariability = <continuous> => is_Real(sv.fmi2ScalarVariable)
		),

		-- @OnFail("%NAME: Variable %s initial/causality %s/%s invalid at %#s",
		-- sv.name, sv.initial, eCausality, sv.location)
		(
			-- Table on p47 defining initial
			sv.initial <> nil =>
				(eCausality not in set {<input>, <independent>})
		),

		-- @OnFail("%NAME: Variable %s initial/variability/start %s/%s/%s invalid at %#s",
		-- sv.name, eInitial, eVariability, sv.fmi2ScalarVariable.start, loc2str(sv.location))
		(
			-- Table on p47 defining initial
			cases eInitial:
				<exact> ->
					sv.fmi2ScalarVariable.start <> nil,

				<approx> ->
					sv.fmi2ScalarVariable.start <> nil
					and eVariability <> <constant>,

				<calculated> ->
					sv.fmi2ScalarVariable.start = nil
					and eVariability <> <constant>,

				nil ->		-- Note that eInitial can be nil (undefined in table on p48)
					true	-- Tests on eInitial above are sufficient
			end
		)
	]);

validDependencyKinds: Unknown +> bool
validDependencyKinds(entry) ==
	entry.dependenciesKind <> nil =>
		-- @OnFail("%NAME: dependencies do not match dependenciesKind at %#s", loc2str(entry.location))
		( entry.dependencies <> nil and len entry.dependenciesKind = len entry.dependencies );

validModelAttributes: FmiModelDescription +> bool
validModelAttributes(md) ==
	-- @OnFail("%NAME: ModelAttribute fmiVersion should be 2.0")
	( md.fmiVersion in set { "2.0" } );

validVendorAnnotations:FmiModelDescription +> bool
validVendorAnnotations(fmd) ==
	let tools = fmd.vendorAnnotations in
		tools <> nil =>
			-- @OnFail("%NAME: VendorAnnotations tool names are not unique: %s",
			--	{ tools(a) | a, b in set inds tools & a <> b and tools(a) = tools(b) })
			( card { name | name in seq tools } = len tools );

validModelTypes: FmiModelDescription +> bool
validModelTypes(fmd) ==
	-- @OnFail("%NAME: Either ModelExchange or CoSimulation must be defined")
	( fmd.modelExchange <> nil or fmd.coSimulation <> nil );

validGenerationDateAndTime: FmiModelDescription +> bool
validGenerationDateAndTime(fmd) ==
	-- @OnFail("%NAME: generationDateAndTime should be YYYY-MM-DDThh:mm:ssZ at %#s",
	-- loc2str(fmd.location))
	( fmd.generationDateAndTime <> nil => iso8601(fmd.generationDateAndTime) );

validTypeUnits: FmiModelDescription +> bool
validTypeUnits(fmd) ==
	fmd.typeDefinitions <> nil => allOf
	([
		tdef.fmi2SimpleType.unit <> nil =>
			-- @OnFail("%NAME: Type %s, unit %s not defined in UnitDefinitions at %#s",
			-- tdef.name, tdef.fmi2SimpleType.unit, loc2str(tdef.location))
			( fmd.unitDefinitions <> nil
				and exists u in seq fmd.unitDefinitions & u.name = tdef.fmi2SimpleType.unit )

		| tdef in seq fmd.typeDefinitions & is_Real(tdef.fmi2SimpleType)
	]);

validVariableTypes: FmiModelDescription +> bool
validVariableTypes(fmd) == allOf
	([
		mv.fmi2ScalarVariable.declaredType <> nil =>
		let tdef = lookupType(mv.fmi2ScalarVariable.declaredType, fmd.typeDefinitions) in
			-- @OnFail("%NAME: %s type %s not found at %#s",
			-- mv.name, mv.fmi2ScalarVariable.declaredType, loc2str(mv.location))
			( tdef <> nil )

			-- @OnFail("%NAME: %s type %s mismatch at %#s",
			-- mv.name, mv.fmi2ScalarVariable.declaredType, loc2str(mv.location))
			and ( kindOf(tdef.fmi2SimpleType) = kindOf(mv.fmi2ScalarVariable) )

		| mv in seq fmd.modelVariables
	]);

validTypeNames: FmiModelDescription +> bool
validTypeNames(fmd) == fmd.typeDefinitions <> nil => allOf
	([
		-- @OnFail("%NAME: TypeDefinition and Variable names overlap: %s at %#s",
		-- tdef.name, loc2str(tdef.location))
		( not exists mv in seq fmd.modelVariables & mv.name = tdef.name )

		| tdef in seq fmd.typeDefinitions
	]);

validVariableNames: FmiModelDescription +> bool
validVariableNames(fmd) ==
	fmd.variableNamingConvention = <structured> => allOf(conc
	[
		[
			-- @OnFail("%NAME: Structured name %s invalid at %#s", mv.name, loc2str(mv.location))
			( validStructuredName(mv.name) ),

			-- @OnFail("%NAME: Name %s is not Real at %#s", mv.name, loc2str(mv.location))
			( mv.name(1, ..., 4) = "der(" => is_Real(mv.fmi2ScalarVariable) )
		]

		| mv in seq fmd.modelVariables
	]);

validStart: FmiModelDescription * ModelVariables +> bool
validStart(-, evs) == allOf
	([
		let type = ev.fmi2ScalarVariable in
		[
			type.start <> nil =>
				-- @OnFail("%NAME: all start values must be between %s and %s at %#s",
				-- ev.fmi2ScalarVariable.min, ev.fmi2ScalarVariable.max, loc2str(ev.location))
				( type.min <= type.start and type.max >= type.start ),

			type.start = nil and ev.initial <> <calculated> =>
				-- @OnFail("%NAME: Warning: implicit start of 0 not within min/max at %#s",
				-- loc2str(ev.location))
				( (type.min <> nil => type.min <= 0) and
				  (type.max <> nil => type.max >= 0) ) or true	-- NOTE warning
		]

		| ev in seq evs & is_MinMaxType(ev.fmi2ScalarVariable)
	]);

validMinMax: FmiModelDescription * ModelVariables +> bool
validMinMax(fmd, evs) == allOf
	([
		let type = ev.fmi2ScalarVariable,
			tdef = lookupType(type.declaredType, fmd.typeDefinitions),
			mk_(kmin, kmax) = minMaxOfKind(kindOf(type)) in
		[
			-- @OnFail("%NAME: max %s is not a valid value of this type", type.max)
			( type.max <= kmax and type.max >= kmin ),

			-- @OnFail("%NAME: min %s is not a valid value of this type", type.min)
			( type.min <= kmax and type.min >= kmin ),

			-- @OnFail("%NAME: max %s not >= min %s", type.max, type.min)
			( type.max >= type.min ),

			-- @OnFail(1034, "%NAME: ScalarVariable %s min/max exceeds RealType %s at %#s",
			-- ev.name, ev.fmi2ScalarVariable.declaredType, loc2str(ev.location))
			( tdef <> nil and tdef.fmi2SimpleType.min <> nil and type.min <> nil =>
				tdef.fmi2SimpleType.min <= type.min ),

			-- @OnFail(1034, "%NAME: ScalarVariable %s min/max exceeds RealType %s at %#s",
			-- ev.name, ev.fmi2ScalarVariable.declaredType, loc2str(ev.location))
			( tdef <> nil and tdef.fmi2SimpleType.max <> nil and type.max <> nil =>
				tdef.fmi2SimpleType.max >= type.max )
		]

		| ev in seq evs & is_MinMaxType(ev.fmi2ScalarVariable)
	]);

validMultipleSets: FmiModelDescription * ModelVariables +> bool
validMultipleSets(fmd, evs) == allOf
	([
		ev.canHandleMultipleSetPerTimeInstant = true =>
			-- @OnFail("%NAME: Variable %s, canHandleMultipleSetPerTimeInstant invalid at %#s",
			-- ev.name, loc2str(ev.location))
			( fmd.modelExchange <> nil and ev.causality = <input> )

		| ev in seq evs
	]);

validReinits: FmiModelDescription +> bool
validReinits(fmd) == allOf
	([
		let mv = fmd.modelVariables(i) in
			is_Real(mv.fmi2ScalarVariable) and mv.fmi2ScalarVariable.reinit <> nil =>
				-- @OnFail("%NAME: %s, Real reinit for model exchange continuous time only at %#s",
				-- mv.name, loc2str(mv.location))
				( isContinuousTimeState(i, fmd.modelVariables) and fmd.modelExchange <> nil )

		| i in set inds fmd.modelVariables
	]);

validVariableUnits: FmiModelDescription * ModelVariables +> bool
validVariableUnits(fmd, evs) == allOf
([
	is_Real(sv.fmi2ScalarVariable) => allOf
	([
		-- @OnFail("%NAME: ScalarVariable %s, Real unit must be defined for displayUnit %s at %#s",
		--	sv.name, sv.fmi2ScalarVariable.displayUnit, loc2str(sv.location))
		( sv.fmi2ScalarVariable.displayUnit <> nil => sv.fmi2ScalarVariable.unit <> nil ),

		sv.fmi2ScalarVariable.unit <> nil =>
			-- @OnFail("%NAME: ScalarVariable %s, Real unit %s not defined in UnitDefinitions at %#s",
			--	sv.name, sv.fmi2ScalarVariable.unit, loc2str(sv.location))
			( fmd.unitDefinitions <> nil
				and exists u in seq fmd.unitDefinitions & u.name = sv.fmi2ScalarVariable.unit )
	])

	| sv in seq evs
]);

validOutputs: FmiModelDescription * ModelVariables +> bool
validOutputs(fmd, evs) ==
	let outputIndexes = { svi | svi in set inds evs & evs(svi).causality = <output> } in
		if outputIndexes <> {}
		then
			-- @OnFail("%NAME: Output variables but no outputs declared at %#s",
			--	loc2str(fmd.modelStructure.location))
			( fmd.modelStructure.outputs <> nil )

			and let structIndexes = { u.index | u in seq fmd.modelStructure.outputs } in allOf
			([

				-- @OnFail("%NAME: Outputs section does not match output variables at %#s",
				--	loc2str(fmd.modelStructure.location))
				( structIndexes = outputIndexes ),

				-- @OnFail("%NAME: Output indexes out of range at %#s",
				--	loc2str(fmd.modelStructure.location))
				( forall i in set structIndexes & i <= len evs )
			])
		else
			-- @OnFail("%NAME: Outputs should be omitted at %#s",
			--	loc2str(fmd.modelStructure.location))
			( fmd.modelStructure.outputs = nil );

validDerivatives: FmiModelDescription * ModelVariables +> bool
validDerivatives(fmd, evs) ==
	fmd.modelExchange <> nil
	or (fmd.coSimulation <> nil and fmd.coSimulation.providesDirectionalDerivative = true) =>
		fmd.modelStructure.derivatives <> nil => allOf
		([
			-- @OnFail("%NAME: Derivative index out of range at %#s", loc2str(u.location))
			( u.index <= len evs )

			and let sv = evs(u.index) in allOf
			([
				-- @OnFail("%NAME: SV not a state derivative at %#s", loc2str(u.location))
				( isStateDerivative(sv) ),

				-- @OnFail("%NAME: Derivative must be continuous at %#s", loc2str(u.location))
				( u.dependencies <> nil => sv.variability = <continuous> )
			])

			| u in seq fmd.modelStructure.derivatives
		]);

validInitialUnknowns: FmiModelDescription * ModelVariables +> bool
validInitialUnknowns(fmd, evs) ==
	let ctVars = continuousTimeStates(evs),
		sdVars = stateDerivatives(evs),
		initIndexes = { svi | svi in set inds evs &
			let sv = evs(svi) in
				(sv.causality = <output>
					and sv.initial in set { <approx>, <calculated> })

				or (sv.causality = <calculatedParameter>)

				or (sv in set ctVars
					and sv.initial in set { <approx>, <calculated> })

				or (sv in set sdVars
					and sv.initial in set { <approx>, <calculated> }) }
	in
		initIndexes <> {} =>
			let ius = fmd.modelStructure.initialUnknowns in allOf
			([
				-- @OnFail("%NAME: InitialUnknowns must include: %s", initIndexes)
				( ius <> nil ),

				-- @OnFail("%NAME: InitialUnknowns must not include: %s",
				-- { u.index | u in seq ius } \ initIndexes )
				( ius <> nil => { u.index | u in seq ius } subset initIndexes ),

				-- @OnFail("%NAME: InitialUnknowns are not sorted: %s",
				-- [ u.index | u in seq ius ])
				( ius <> nil =>
						forall i in set inds ius &
							i = len ius or ius(i).index < ius(i+1).index )
			]);

validCompilerOptions: SourceFileSet +> bool
validCompilerOptions(sfs) ==
	-- @OnFail("%NAME: Compiler options set without compiler at %#s", loc2str(sfs.location))
	( sfs.compilerOptions <> nil => sfs.compiler <> nil );

validSourceFileNames: SourceFileSet +> bool
validSourceFileNames(sfs) ==
	let files = sfs.sourceFile in
	let names = [ sf.name | sf in seq files ] in
		-- @OnFail("%NAME: SourceFileSet has duplicate names: %s",
		--	{ files(a) | a, b in set inds names & a <> b and files(a) = files(b) })
		( card elems names = len names );

validPreprocessorDefinitionNames: SourceFileSet +> bool
validPreprocessorDefinitionNames(sfs) ==
	let defs = sfs.preprocessorDefinition in
	defs <> nil =>
		let names = [ d.name | d in seq defs ] in
			-- @OnFail("%NAME: PreprocessorDefinitions has duplicate names: %s",
			--	{ names(a) | a, b in set inds names & a <> b and names(a) = names(b) })
			( card elems names = len names );

validIncludeDirectoryNames: SourceFileSet +> bool
validIncludeDirectoryNames(sfs) ==
	let incs = sfs.includeDirectory in
	incs <> nil =>
		let names = [ d.name | d in seq incs ] in
			-- @OnFail("%NAME: IncludeDirectories has duplicate names: %s",
			--	{ names(a) | a, b in set inds names & a <> b and names(a) = names(b) })
			( card elems names = len names );

validCoordinateSystem: CoordinateSystem +> bool
validCoordinateSystem(cs) == allOf
	([
		-- @OnFail("%NAME: Coordinate system has zero area at %#s", loc2str(cs.location))
		( cs.x1 <> cs.x2 and cs.y1 <> cs.y2 ),

		-- @OnFail("%NAME: Coordinate system is not bottom left to top right at %#s",
		-- loc2str(cs.location))
		( isBLtoTR(cs.x1, cs.y1, cs.x2, cs.y2) )
	]);

validIcon: Icon +> bool
validIcon(icon) ==
	-- @OnFail("%NAME: Icon has zero area at %#s", loc2str(icon.location))
	( icon.x1 <> icon.x2 and icon.y1 <> icon.y2 );

validTerminalMemberVariables: Terminal * [FmiModelDescription] +> bool
validTerminalMemberVariables(terminal, fmd) ==
	let tmvs = terminal.terminalMemberVariable in
	tmvs <> nil and fmd <> nil => allOf
	([
		let var = lookupVariableName(tmv.variableName, fmd.modelVariables) in
			-- @OnFail("%NAME: Terminal member variable %s not declared at %#s",
			-- tmv.variableName, loc2str(tmv.location))
			( var <> nil )

		| tmv in seq tmvs
	]);

validTerminalStreamMemberVariables: Terminal * [FmiModelDescription] +> bool
validTerminalStreamMemberVariables(terminal, fmd) ==
	let tsmvs = terminal.terminalStreamMemberVariable in
	tsmvs <> nil and fmd <> nil =>allOf
	([
		let ivar = lookupVariableName(tsmv.inStreamVariableName, fmd.modelVariables),
			ovar = lookupVariableName(tsmv.outStreamVariableName, fmd.modelVariables)
		in
		[
			-- @OnFail("%NAME: Terminal inStreamVariableName %s not declared at %#s",
			-- tsmv.inStreamVariableName, loc2str(tsmv.location))
			( ivar <> nil ),

			-- @OnFail("%NAME: Terminal outStreamVariableName %s not declared at %#s",
			-- tsmv.outStreamVariableName, loc2str(tsmv.location))
			( ovar <> nil )
		]

		| tsmv in seq tsmvs
	]);

validTerminalGraphicalRepresentation: Terminal +> bool
validTerminalGraphicalRepresentation(terminal) ==
	let tgr = terminal.terminalGraphicalRepresentation in
	tgr <> nil => allOf
	([
		-- @OnFail("%NAME: Terminal area is zero at %#s", loc2str(tgr.location))
		( tgr.x1 <> tgr.x2 and tgr.y1 <> tgr.y2 ),

		-- @OnFail("%NAME: Colour attributes must be octets (<=255) at %#s",
		-- loc2str(tgr.location))
		( tgr.defaultConnectionColor <> nil =>
			forall c in seq tgr.defaultConnectionColor & c <= 255 ),

		-- @OnFail("%NAME: defaultConnectionStrokeSize must be >0 at %#s",
		-- loc2str(tgr.location))
		( tgr.defaultConnectionStrokeSize <> nil =>
			tgr.defaultConnectionStrokeSize > 0 )
	]);