`refine_plan.models.condition`

Classes for PRISM conditions and state labels.

Author: Charlie Street Owner: Charlie Street

Module Contents

Classes

`Label`	A PRISM label is a condition with a name.
`Condition`	Base class for conditions.
`TrueCondition`	A condition which is always true.
`EqCondition`	A condition which checks for equality.
`NeqCondition`	A condition which checks if a state factor is not equal to a value.
`NotCondition`	A condition which negates another condition.
`AddCondition`	Condition for adding a value to a state factor.
`InequalityCondition`	A precondition which compares a state factor to a value.
`LtCondition`	A precondition for <.
`GtCondition`	A precondition for >.
`LeqCondition`	A precondition for <=.
`GeqCondition`	A precondition for >=.
`AndCondition`	Composite condition which captures conjunctions.
`OrCondition`	Composite condition which captures disjunctions.

class refine_plan.models.condition.Label(name, cond)

Bases: object

A PRISM label is a condition with a name.

_name: The label name

_cond: The corresponding condition

_hash_val: The cached hash value for the label

to_prism_string()

Converts the label into a PRISM string.

Returns:: The corresponding PRISM string

class refine_plan.models.condition.Condition

Bases: object

Base class for conditions.

Condition objects directly correspond to conditions in PRISM.

abstract is_satisfied(state, prev_state=None)

Checks if a state satisfies a given condition.

Parameters:

state – The state to check
prev_state – The previous state (necessary for some post conditions)

Returns:

Is the condition satisfied?

abstract is_pre_cond()

Returns True if condition can be used as a precondition.

Returns:: Can the condition be used as a precondition?

abstract is_post_cond()

Returns True if condition can be used as a postcondition.

Returns:: Can the condition be used as a postcondition?

abstract to_prism_string(is_post_cond=False)

Outputs the prism string for this condition.

Parameters:: is_post_cond – Should the condition be written as a postcondition?

abstract to_pyeda_expr()

Converts the condition into a pyeda logical expression.

This allows it to be worked with and minimised etc.

Returns:

The corresponding pyeda expression
A mapping from var_name to condition. Only returned if return_var_map

abstract range_of_values()

Returns the range of values that can be satisfied with this condition.

Returns:: A list of dictionaries from state factor to a list of values

class refine_plan.models.condition.TrueCondition

Bases: Condition

A condition which is always true.

is_satisfied(state, prev_state=None)

Always returns True.

Parameters:

state – Not used
prev_state – Not used

Returns:

Always True

is_pre_cond()

TrueCondition is a valid precondition

Returns:: True

is_post_cond()

TrueConditions can be used to signify self loops in PRISM

Returns:: True for TrueConditions

to_prism_string(is_post_cond=False)

Outputs the prism string for this condition.

Parameters:: is_post_cond – Should the condition be written as a postcondition?

to_pyeda_expr()

Converts the condition into a pyeda logical expression (1)

Returns:

The corresponding pyeda expression
A mapping from var_name to condition.

range_of_values()

Raises exception as it is impossible to return everything.

Raises:: cant_return_everything – Raised as there is no range as its everything

class refine_plan.models.condition.EqCondition(sf, value)

Bases: Condition

A condition which checks for equality.

_sf: The state factor we’re checking

_value: The value to check against

_hash_val: The cached hash

is_satisfied(state, prev_state=None)

Checks if the value of _sf in state matches _value.

Parameters:

state – The state to check
prev_state – Not used here

Returns:

Is the condition satisfied?

Raises:

invalid_value – Raised if state has an invalid value for _sf

is_pre_cond(): EqConditions are valid preconditions. :returns: Can the condition be used as a precondition?

is_post_cond()

EqConditions are valid postconditions.

Returns:: Can the condition be used as a postcondition?

to_prism_string(is_post_cond=False)

Outputs the prism string for this condition.

Parameters:: is_post_cond – Should the condition be written as a postcondition?

to_pyeda_expr()

Converts the condition into a pyeda logical expression.

We create a variable name for the condition <sf_name>EQ<value>.

Returns:

The corresponding pyeda expression
A mapping from var_name to condition.

range_of_values()

Return the one value that satisfies this condition.

Returns:: The range of values (the one value) that satisfies the condition

class refine_plan.models.condition.NeqCondition(sf, value)

Bases: Condition

A condition which checks if a state factor is not equal to a value.

_sf: The state factor we’re checking

_value: The value to check against

_hash_val: The cached hash

is_satisfied(state, prev_state=None)

Checks if the value of _sf in state matches _value.

Parameters:

state – The state to check
prev_state – Not used here

Returns:

Is the condition satisfied?

Raises:

invalid_value – Raised if state has an invalid value for _sf

is_pre_cond(): NeqConditions are valid preconditions. :returns: Can the condition be used as a precondition?

is_post_cond()

NeqConditions are not valid postconditions.

Returns:: Can the condition be used as a postcondition?

to_prism_string(is_post_cond=False)

Outputs the prism string for this condition.

Parameters:: is_post_cond – Should the condition be written as a postcondition?

to_pyeda_expr()

Converts the condition into a pyeda logical expression.

We don’t want to create variables like sfNEQval here, as it might get confused as being different to Not(EqCondition), which is equivalent. Therefore, we create a variable for the flipped EQCondition and use a not operator.

Returns:

The corresponding pyeda expression
A mapping from var_name to condition.

range_of_values()

Returns the state factor values without self._value.

Returns:: The range of values that satisfy the condition.

class refine_plan.models.condition.NotCondition(cond)

Bases: Condition

A condition which negates another condition.

_cond: The condition we’re negating

_hash_val: The cached hash

is_satisfied(state, prev_state=None)

Flips the return value of self._cond

Parameters:

state – The state to check
prev_state – Not used here

Returns:

Is the condition satisfied?

is_pre_cond(): NotConditions are valid preconditions. :returns: Can the condition be used as a precondition?

is_post_cond()

NotConditions are not valid postconditions.

Returns:: Can the condition be used as a postcondition?

to_prism_string(is_post_cond=False)

Outputs the prism string for this condition.

Parameters:: is_post_cond – Should the condition be written as a postcondition?

to_pyeda_expr()

Converts the condition into a pyeda logical expression.

This just negates the condition included in the object.

Returns:

The corresponding pyeda expression
A mapping from var_name to condition.

abstract range_of_values(): Raises NotImplementedError as not needed currently.

class refine_plan.models.condition.AddCondition(sf, inc_value)

Bases: Condition

Condition for adding a value to a state factor.

Only valid for IntStateFactors.

Same as superclass, plus

_sf: The state factor

_inc_value: The increment value

_hash_val: The cached hash

is_satisfied(state, prev_state=None)

Checks if the value of _sf in state = prev_state + _inc_value

Parameters:

state – The state to check
prev_state – The previous state

Returns:

Is the condition satisfied?

Raises:

invalid_value – Raised if the incremented value is out of bounds
no_prev_state – Raised if prev_state not specified

is_pre_cond(): AddConditions are not valid preconditions. :returns: Can the condition be used as a precondition?

is_post_cond()

AdsConditions are valid postconditions.

Returns:: Can the condition be used as a postcondition?

to_prism_string(is_post_cond=False)

Outputs the prism string for this condition.

Parameters:: is_post_cond – Should the condition be written as a postcondition?

to_pyeda_expr(): Throws exception as AddConditions are only postconditions.

range_of_values()

Raises Exception as not applicable to AddConditions.

Raises:: not_for_post_cond – Raised as function doesn’t apply to postconditions

class refine_plan.models.condition.InequalityCondition(sf, value, comp_fn, comp_str)

Bases: Condition

A precondition which compares a state factor to a value.

EqCondition is not included here, as it can be a postcondition. This class can (and will) be used for <, >, <=, >=

_sf: The state factor we’re checking

_comp_fn: The int x int -> bool comparison function

_comp_str: The PRISM symbol for the comparison operation

_value: The value to check against

_hash_val: The cached hash

is_satisfied(state, prev_state=None)

Checks if the value of _sf in state matches _value.

Parameters:

state – The state to check
prev_state – Not used here

Returns:

Is the condition satisfied?

Raises:

invalid_value – Raised if state has an invalid value for _sf

is_pre_cond(): InequalityConditions are valid preconditions. :returns: Can the condition be used as a precondition?

is_post_cond()

InequalityConditions are valid postconditions.

Returns:: Can the condition be used as a postcondition?

to_prism_string(is_post_cond=False)

Outputs the prism string for this condition.

Parameters:: is_post_cond – Should the condition be written as a postcondition?
Raises:: post_cond_exception – Raised if is_post_cond is True

range_of_values()

Returns the values which satisfy the inequality.

Returns:: The range of values which satisfy this inequality

class refine_plan.models.condition.LtCondition(sf, value)

Bases: InequalityCondition

A precondition for <.

Same as superclass.

to_pyeda_expr()

Converts the condition into a pyeda logical expression.

We need to be careful with inequalities when minimising. Following from https://github.com/SimonaGug/BT-from-planning-experts < is represented logically as Not(>=). We have a variable for the >= as well, not the < We can then convert this back after doing all the logical work we need.

Returns:

The corresponding pyeda expression
A mapping from var_name to condition

class refine_plan.models.condition.GtCondition(sf, value)

Bases: InequalityCondition

A precondition for >.

Same as superclass.

to_pyeda_expr()

Converts the condition into a pyeda logical expression.

> are represented just as >. Its < and <= which are flipped in terms of variables.

Returns:

The corresponding pyeda expression
A mapping from var_name to condition.

class refine_plan.models.condition.LeqCondition(sf, value)

Bases: InequalityCondition

A precondition for <=.

Same as superclass.

to_pyeda_expr()

Converts the condition into a pyeda logical expression.

We need to be careful with inequalities when minimising. Following from https://github.com/SimonaGug/BT-from-planning-experts <= is represented logically as Not(>). We have a variable for the > as well, not the <= We can then convert this back after doing all the logical work we need.

Returns:

The corresponding pyeda expression
A mapping from var_name to condition.

class refine_plan.models.condition.GeqCondition(sf, value)

Bases: InequalityCondition

A precondition for >=.

Same as superclass.

to_pyeda_expr()

Converts the condition into a pyeda logical expression.

>= are represented just as >=. Its < and <= which are flipped in terms of variables.

Returns:

The corresponding pyeda expression
A mapping from var_name to condition.

class refine_plan.models.condition.AndCondition(*conds)

Bases: Condition

Composite condition which captures conjunctions.

_cond_list: A list of conditions

_hash_val: The cached hash

add_cond(cond)

Add a new condition to the conjunction.

Parameters:: cond – The new condition

is_satisfied(state, prev_state=None)

Check if conjunction is satisfied.

Parameters:

state – The current state to check
prev_state – The previous statem (if needed)

Returns:

True if condition satisfied, else False

is_pre_cond()

Conjunction is pre cond if all conditions are preconditions.

Returns:: True if all conditions are preconditions, else False

is_post_cond()

Conjunction is post cond if all conditions are postconditions.

Returns:: True if all conditions are postconditions, else False

to_prism_string(is_post_cond=False)

Output condition into prism string format.

Parameters:: is_post_cond – Is the condition a post condition?

to_pyeda_expr()

Converts the condition into a pyeda logical expression.

Here we just do an And() of all sub-conditions, and combine the variable maps.

Returns:

The corresponding pyeda expression
A mapping from var_name to condition.

abstract range_of_values(): Raises NotImplementedError as not needed currently.

class refine_plan.models.condition.OrCondition(*conds)

Bases: Condition

Composite condition which captures disjunctions.

_cond_list: A list of conditions

_hash_val: The cached hash

add_cond(cond)

Add a new condition to the conjunction.

Parameters:: cond – The new condition

is_satisfied(state, prev_state=None)

Check if disjunction is satisfied.

Parameters:

state – The current state to check
prev_state – The previous statem (if needed)

Returns:

True if condition satisfied, else False

is_pre_cond()

Disjunction is pre cond if all conditions are preconditions.

Returns:: True if all conditions are preconditions, else False

is_post_cond()

Disjunction cannot be a postcondition.

Returns:: False for disjunctions

to_prism_string(is_post_cond=False)

Output condition into prism string format.

Parameters:: is_post_cond – Is the condition a post condition?

to_pyeda_expr()

Converts the condition into a pyeda logical expression.

Here we just do an Or() of all sub-conditions, and combine the variable maps.

Returns:

The corresponding pyeda expression
A mapping from var_name to condition.

abstract range_of_values(): Raises NotImplementedError as not needed currently.

refine_plan.models.condition

Module Contents

Classes

`refine_plan.models.condition`