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)
    // Array of two-element arrays, each of those representing a bound for some variable
	bounds: [[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",
    // Two dimensional array where each inner array represents a rectangle.
    // Each rectangle is represented by an array of two-element arrays
    // Each of those representing bounds for a specific parameter.
	rectangles: [[[Double]]]	
}

SmtSet : ParameterSet {
	type: "smt",
    rectangles: [{
        rect: [[Double]],    // A p-dimensional array of pairs of Double.
        // A (p*(p-1)/2)-dimensional array of pairs of Double representing 
        // ratios of each combination of p-parameters with format:
        // [d_1,d_2],...,[d_1,d_p],[d_2,d_3],...,[d_(p-1),d_p].
        ratio: [[Double]]
    }]
}