BioDivine Outputs

This page summarises the format of various tools inside the BioDivine framework.

StateSpace {
    states: [State],
    params: [ParameterSet],
    transitions: [Transition]
}

State {
	id: Int, 	// The state indentifier (deterministic)
	bounds: {
		variable: String,
		from: Double,
		to: Double
	}
}

Transition {
	from: Int 		// Index into the states array
	to: Int 		// Index into the states array
	params: Int 	// Index into the params array
}

ResultSet {
	states: [State],
	params: [ParameterSet],
	results: [Result]
}

Result {
	//Note: we might change the String into a json later so that it's 
	//easier to manipulate
	formula: String		// String representation of verified formula 
	data: [{
		state: Int 		// Index into the states array
		param: Int 		// Index into the params array
	}]
}

//ParameterSet can have several types:

RectangularSet : ParameterSet {
	type: "rectangular",
	rectangles: [[Double]]	// Two dimensional array where each inner array represents a rectangle
}

SmtSet : ParameterSet {
	type: "smt"
}