Coco Verification Results¶

AssertionResult¶

One Of:	LeafAssertionResult – GroupAssertionResult –

BaseAssertionResult¶

Properties:	name (String) – The name of the assertion. status (VerificationStatus) – The name of the assertion. cached (Boolean) – Whether the assertion was cached. statistics (VerificationStatistics) –

Counterexample¶

Properties:	text (String) – A textual description of the counterexample.

GroupAssertionResult¶

All Of:	BaseAssertionResult –
Properties:	children (Array[AssertionResult]) – The results of the assertions in this group.

LeafAssertionResult¶

All Of:	BaseAssertionResult –
Properties:	counterexamples (Array[Counterexample]) – Counterexamples that failed the assertion.

Root¶

Properties:	$schema (String) – The schema that this document conforms to.

VerificationStatistics¶

One Of:	VerificationStatisticsExplicitState – VerificationStatisticsLogReplay –

BaseVerificationStatistics¶

Properties:	time (Integer) – The duration of the verification in milliseconds. preparation_time (Integer) – The amount of time spent preparing for verification. This includes time converting the state machines into a form that can be verified.

VerificationStatisticsExplicitState¶

All Of:	BaseVerificationStatistics –
Properties:	states (Integer) – The number of states visited. Use a 64-bit type for this. transitions (Integer) – The number of transitions visited. Use a 64-bit type for this. total_memory_used (Integer) – The total amount of memory required to perform the verification, in bytes. Use a 64-bit type for this.

VerificationStatisticsLogReplay¶

All Of:	BaseVerificationStatistics –
Properties:	lines_processed (Integer) – The number of lines that were actually processed; i.e. contained a valid message that was passed to the log replay. lines_read (Integer) – The number of log lines that were read, including comment and irrelevant lines.