refine_plan.models.condition
============================

.. py:module:: refine_plan.models.condition

.. autoapi-nested-parse::

   Classes for PRISM conditions and state labels.

   Author: Charlie Street
   Owner: Charlie Street



Classes
-------

.. autoapisummary::

   refine_plan.models.condition.Label
   refine_plan.models.condition.Condition
   refine_plan.models.condition.TrueCondition
   refine_plan.models.condition.EqCondition
   refine_plan.models.condition.NeqCondition
   refine_plan.models.condition.NotCondition
   refine_plan.models.condition.AddCondition
   refine_plan.models.condition.InequalityCondition
   refine_plan.models.condition.LtCondition
   refine_plan.models.condition.GtCondition
   refine_plan.models.condition.LeqCondition
   refine_plan.models.condition.GeqCondition
   refine_plan.models.condition.AndCondition
   refine_plan.models.condition.OrCondition


Module Contents
---------------

.. py:class:: Label(name, cond)

   Bases: :py:obj:`object`


   A PRISM label is a condition with a name.

   .. attribute:: _name

      The label name

   .. attribute:: _cond

      The corresponding condition

   .. attribute:: _hash_val

      The cached hash value for the label


   .. py:method:: to_prism_string()

      Converts the label into a PRISM string.

      :returns: The corresponding PRISM string



.. py:class:: Condition

   Bases: :py:obj:`object`


   Base class for conditions.

   Condition objects directly correspond to conditions in PRISM.


   .. py:method:: is_satisfied(state, prev_state=None)
      :abstractmethod:


      Checks if a state satisfies a given condition.

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

      :returns: Is the condition satisfied?



   .. py:method:: is_pre_cond()
      :abstractmethod:


      Returns True if condition can be used as a precondition.

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



   .. py:method:: is_post_cond()
      :abstractmethod:


      Returns True if condition can be used as a postcondition.

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



   .. py:method:: to_prism_string(is_post_cond=False)
      :abstractmethod:


      Outputs the prism string for this condition.

      :param is_post_cond: Should the condition be written as a postcondition?



   .. py:method:: to_pyeda_expr()
      :abstractmethod:


      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



   .. py:method:: to_scxml_cond(is_post_cond=False)
      :abstractmethod:


      Outputs the SCXML condition for this condition.

      If is_post_cond=False, we output a JavaScript style condition string
      If is_post_cond=True, we output a list of <assign/> SCXML elements

      :param is_post_cond: Is the condition a postcondition?



   .. py:method:: range_of_values()
      :abstractmethod:


      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



.. py:class:: TrueCondition

   Bases: :py:obj:`Condition`


   A condition which is always true.


   .. py:method:: is_satisfied(state, prev_state=None)

      Always returns True.

      :param state: Not used
      :param prev_state: Not used

      :returns: Always True



   .. py:method:: is_pre_cond()

      TrueCondition is a valid precondition

      :returns: True



   .. py:method:: is_post_cond()

      TrueConditions can be used to signify self loops in PRISM

      :returns: True for TrueConditions



   .. py:method:: to_prism_string(is_post_cond=False)

      Outputs the prism string for this condition.

      :param is_post_cond: Should the condition be written as a postcondition?



   .. py:method:: to_pyeda_expr()

      Converts the condition into a pyeda logical expression (1)

      :returns:

                - The corresponding pyeda expression
                - A mapping from var_name to condition.



   .. py:method:: to_scxml_cond(is_post_cond=False)

      Return None for both. A TrueCondition doesn't make much sense here

      :param is_post_cond: Is the condition a postcondition?



   .. py:method:: 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



.. py:class:: EqCondition(sf, value)

   Bases: :py:obj:`Condition`


   A condition which checks for equality.

   .. attribute:: _sf

      The state factor we're checking

   .. attribute:: _value

      The value to check against

   .. attribute:: _hash_val

      The cached hash


   .. py:method:: is_satisfied(state, prev_state=None)

      Checks if the value of _sf in state matches _value.

      :param state: The state to check
      :param prev_state: Not used here

      :returns: Is the condition satisfied?

      :raises invalid_value: Raised if state has an invalid value for _sf



   .. py:method:: is_pre_cond()

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



   .. py:method:: is_post_cond()

      EqConditions are valid postconditions.

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



   .. py:method:: to_prism_string(is_post_cond=False)

      Outputs the prism string for this condition.

      :param is_post_cond: Should the condition be written as a postcondition?



   .. py:method:: 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.



   .. py:method:: to_scxml_cond(is_post_cond=False)

      Return an equality string or a single XML assignment.

      :param is_post_cond: Is the condition a postcondition?



   .. py:method:: range_of_values()

      Return the one value that satisfies this condition.

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



.. py:class:: NeqCondition(sf, value)

   Bases: :py:obj:`Condition`


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

   .. attribute:: _sf

      The state factor we're checking

   .. attribute:: _value

      The value to check against

   .. attribute:: _hash_val

      The cached hash


   .. py:method:: is_satisfied(state, prev_state=None)

      Checks if the value of _sf in state matches _value.

      :param state: The state to check
      :param prev_state: Not used here

      :returns: Is the condition satisfied?

      :raises invalid_value: Raised if state has an invalid value for _sf



   .. py:method:: is_pre_cond()

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



   .. py:method:: is_post_cond()

      NeqConditions are not valid postconditions.

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



   .. py:method:: to_prism_string(is_post_cond=False)

      Outputs the prism string for this condition.

      :param is_post_cond: Should the condition be written as a postcondition?



   .. py:method:: 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.



   .. py:method:: to_scxml_cond(is_post_cond=False)

      Return an not equal string or an Exception if post condition.

      :param is_post_cond: Is the condition a postcondition?



   .. py:method:: range_of_values()

      Returns the state factor values without self._value.

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



.. py:class:: NotCondition(cond)

   Bases: :py:obj:`Condition`


   A condition which negates another condition.

   .. attribute:: _cond

      The condition we're negating

   .. attribute:: _hash_val

      The cached hash


   .. py:method:: is_satisfied(state, prev_state=None)

      Flips the return value of self._cond

      :param state: The state to check
      :param prev_state: Not used here

      :returns: Is the condition satisfied?



   .. py:method:: is_pre_cond()

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



   .. py:method:: is_post_cond()

      NotConditions are not valid postconditions.

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



   .. py:method:: to_prism_string(is_post_cond=False)

      Outputs the prism string for this condition.

      :param is_post_cond: Should the condition be written as a postcondition?



   .. py:method:: 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.



   .. py:method:: to_scxml_cond(is_post_cond=False)

      Return a ! string or an exception if post condition.

      :param is_post_cond: Is the condition a postcondition?



   .. py:method:: range_of_values()
      :abstractmethod:


      Raises NotImplementedError as not needed currently.



.. py:class:: AddCondition(sf, inc_value)

   Bases: :py:obj:`Condition`


   Condition for adding a value to a state factor.

   Only valid for IntStateFactors.

   .. attribute:: Same as superclass, plus

      

   .. attribute:: _sf

      The state factor

   .. attribute:: _inc_value

      The increment value

   .. attribute:: _hash_val

      The cached hash


   .. py:method:: is_satisfied(state, prev_state=None)

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

      :param state: The state to check
      :param prev_state: The previous state

      :returns: Is the condition satisfied?

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



   .. py:method:: is_pre_cond()

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



   .. py:method:: is_post_cond()

      AdsConditions are valid postconditions.

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



   .. py:method:: to_prism_string(is_post_cond=False)

      Outputs the prism string for this condition.

      :param is_post_cond: Should the condition be written as a postcondition?



   .. py:method:: to_pyeda_expr()

      Throws exception as AddConditions are only postconditions.



   .. py:method:: to_scxml_cond(is_post_cond=False)

      Not implemented as I'm not sure this is supported in SCXML.

      Our representation uses indexes, so there's not a nice way we can use
      this here.

      :param is_post_cond: Is the condition a postcondition?



   .. py:method:: range_of_values()

      Raises Exception as not applicable to AddConditions.

      :raises not_for_post_cond: Raised as function doesn't apply to postconditions



.. py:class:: InequalityCondition(sf, value, comp_fn, comp_str)

   Bases: :py:obj:`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 <, >, <=, >=

   .. attribute:: _sf

      The state factor we're checking

   .. attribute:: _comp_fn

      The int x int -> bool comparison function

   .. attribute:: _comp_str

      The PRISM symbol for the comparison operation

   .. attribute:: _value

      The value to check against

   .. attribute:: _hash_val

      The cached hash


   .. py:method:: is_satisfied(state, prev_state=None)

      Checks if the value of _sf in state matches _value.

      :param state: The state to check
      :param prev_state: Not used here

      :returns: Is the condition satisfied?

      :raises invalid_value: Raised if state has an invalid value for _sf



   .. py:method:: is_pre_cond()

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



   .. py:method:: is_post_cond()

      InequalityConditions are valid postconditions.

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



   .. py:method:: to_prism_string(is_post_cond=False)

      Outputs the prism string for this condition.

      :param is_post_cond: Should the condition be written as a postcondition?

      :raises post_cond_exception: Raised if is_post_cond is True



   .. py:method:: to_scxml_cond(is_post_cond=False)

      Returns a string with the condition if precondition.

      :param is_post_cond: Is the condition a postcondition?



   .. py:method:: range_of_values()

      Returns the values which satisfy the inequality.

      :returns: The range of values which satisfy this inequality



.. py:class:: LtCondition(sf, value)

   Bases: :py:obj:`InequalityCondition`


   A precondition for <.

   .. attribute:: Same as superclass.

      


   .. py:method:: 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



.. py:class:: GtCondition(sf, value)

   Bases: :py:obj:`InequalityCondition`


   A precondition for >.

   .. attribute:: Same as superclass.

      


   .. py:method:: 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.



.. py:class:: LeqCondition(sf, value)

   Bases: :py:obj:`InequalityCondition`


   A precondition for <=.

   .. attribute:: Same as superclass.

      


   .. py:method:: 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.



.. py:class:: GeqCondition(sf, value)

   Bases: :py:obj:`InequalityCondition`


   A precondition for >=.

   .. attribute:: Same as superclass.

      


   .. py:method:: 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.



.. py:class:: AndCondition(*conds)

   Bases: :py:obj:`Condition`


   Composite condition which captures conjunctions.

   .. attribute:: _cond_list

      A list of conditions

   .. attribute:: _hash_val

      The cached hash


   .. py:method:: add_cond(cond)

      Add a new condition to the conjunction.

      :param cond: The new condition



   .. py:method:: is_satisfied(state, prev_state=None)

      Check if conjunction is satisfied.

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

      :returns: True if condition satisfied, else False



   .. py:method:: is_pre_cond()

      Conjunction is pre cond if all conditions are preconditions.

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



   .. py:method:: is_post_cond()

      Conjunction is post cond if all conditions are postconditions.

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



   .. py:method:: to_prism_string(is_post_cond=False)

      Output condition into prism string format.

      :param is_post_cond: Is the condition a post condition?



   .. py:method:: 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.



   .. py:method:: to_scxml_cond(is_post_cond=False)

      Return list of elements or string with escaped & characters.

      :param is_post_cond: Is the condition a post condition?



   .. py:method:: range_of_values()
      :abstractmethod:


      Raises NotImplementedError as not needed currently.



.. py:class:: OrCondition(*conds)

   Bases: :py:obj:`Condition`


   Composite condition which captures disjunctions.

   .. attribute:: _cond_list

      A list of conditions

   .. attribute:: _hash_val

      The cached hash


   .. py:method:: add_cond(cond)

      Add a new condition to the conjunction.

      :param cond: The new condition



   .. py:method:: is_satisfied(state, prev_state=None)

      Check if disjunction is satisfied.

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

      :returns: True if condition satisfied, else False



   .. py:method:: is_pre_cond()

      Disjunction is pre cond if all conditions are preconditions.

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



   .. py:method:: is_post_cond()

      Disjunction cannot be a postcondition.

      :returns: False for disjunctions



   .. py:method:: to_prism_string(is_post_cond=False)

      Output condition into prism string format.

      :param is_post_cond: Is the condition a post condition?



   .. py:method:: 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.



   .. py:method:: to_scxml_cond(is_post_cond=False)

      Return list of elements or string with || characters.

      :param is_post_cond: Is the condition a post condition?



   .. py:method:: range_of_values()
      :abstractmethod:


      Raises NotImplementedError as not needed currently.