BioDivine Outputs

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

StateSpace {
    variables: [String],     // Array of variables names
    thresholds: [[Double]]   // Array where each element is an array of thresholds for particular variable
    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 {
    variables: [String],     // Array of variables names
    parameters: [String],
    thresholds: [[Double]],   // Array where each element is an array of thresholds for particular variable
	states: [State],
	type: "rectangular"/"smt",
	parameter_values: [ParameterSet],
    parameter_bounds: [[Double]],   // Array where each element is an array of two bounds for particular parameter
	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 = [[[Double]]]
RectangularSet : ParameterSet {
    // 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 {
    rectangles: [{
        rect: [[Double]],    // A p-element array of pairs of Double, where p is number of parameters.
        // A (p*(p-1)/2)-element 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]
        // where each d_x is of type Double.
        ratio: [[Double]],
        formula: String       // SMT Lib 2 string
    }]
}