Analysis

CTL

class eBCSgen.Analysis.CTL.CTL

Bases: object

static model_checking(ts: TransitionSystem, CTL_formula: Formula)

Model checking of given CTL formula.

First, a Kripe structure is generated from given transition system and then pyModelChecking model checker is called and results are returned.

Parameters:

ts – given transition system
CTL_formula – given CTL formula

Returns:

output of the model checker

PCTL

class eBCSgen.Analysis.PCTL.PCTL

Bases: object

static model_checking(ts: TransitionSystem, PCTL_formula: Formula)

Model checking of given PCTL formula.

First, Storm explicit file is generated from given transition system and appropriate PCTL formula issues are resolved (e.g. naming of agents). Finally, Storm model checker is called and results are returned.

Parameters:

ts – given transition system
PCTL_formula – given PCTL formula

Returns:

output of Storm model checker

static parameter_synthesis(ts: TransitionSystem, PCTL_formula: Formula, region: str)

Parameter synthesis of given PCTL formula in given region.

First, Storm explicit file is generated from given transition system and appropriate PCTL formula issues are resolved (e.g. naming of agents). Finally, Storm model checker is called and results are returned.

Parameters:

ts – given transition system
PCTL_formula – given PCTL formula
region – string representation of region which will be checked by Storm

Returns:

output of Storm model checker

static process_output(result)

eBCSgen.Analysis.PCTL.call_storm(command: str)

Calls Storm model checker locally.

Parameters:: command – given command to be executed
Returns:: result of Storm execution