First Steps

We introduce in this section the introductory steps which need to be undertaken in order to exploit the functionality of PyIDF.

Here we’ll present a simple but complete example of applying imandra region decomposition to a supervised learning problem with generated input data. We will write a state-tranistion model for a sequence-to-sequence addition problem. Then we will use imandra.idf to create region-based sampling and

First we define two enum types: the Status enum will describe the overall state our adder and the Op enum will encode the next incoming character type:

from enum import Enum, unique
    
@unique
class Status(Enum):
    first   = 0
    second  = 1
    finished = 2

@unique
class Op(Enum):
    digit  = 0
    plus   = 1
    end    = 2

Next, we define the State class. The Python State class definition must be at the core of each Python model we want to decompose. All the values stored in the state must be declared in the __init__ constructor of the class:

class State:
    def __init__(self):
        self.status : Status = Status.first
        self.factor : int = 1
        self.op1 : int = 0
        self.op2 : int = 0
        self.result : int = 0

We’ve declared five state variables:

  • two integer operands op1 and op2
  • the overall status of the model of our Status(Enum) type
  • the integer factor that will be multiplied by 10 with each next incoming character
  • and the result of the addition that we’ll calculate upon receiving the Op.end action Note that for each variable we’ve provided an initial value and its type via Python’s type hints. Both initial values and types are required if you want to decompose the model.

State transitions happen by processing incoming actions. We define incoming actions via State class methods - the names of such methods must start with receive_ followed by the name of your action. Let’s create a Char action, that passes an Op character type and an integer value for the digit:

    def receive_Char(self, op : Op, digit : int):
        if self.status == Status.finished:
            return            
        if op == Op.plus:
            self.state : Status = Status.second
            self.factor : int = 1
        elif op == Op.digit and self.status == Status.first:
            self.op1 : int = self.op1 + digit * self.factor 
            self.factor : int = 10 * self.factor              
        elif op == Op.digit and self.status == Status.second:
            self.op2 : int = self.op2 + digit * self.factor 
            self.factor : int = 10 * self.factor  
        elif op == Op.end:
            self.result : int = self.op1 + self.op2
            self.status : Status = Status.finished

In the receive_Char method we are processing the incoming values and change the state variables accordingly:

  • if op is Op.digit, we increase an operand value by digit * self.factor and multiply the factor by 10
  • if op is Op.plus, we reset the self.factor and move to the second operand
  • if op is Op.end, we compute the sum of the operands and go into the Status.finished
  • if the overall status is finished we ignore all the incoming actions

You might have noticed that for this transition rules to work, certain constraints on incoming values of op and digit must be satisfied. For example, we cannot receive an action with Op.end if we have self.status == Status.first. Similarly, we cannot receive Op.plus if we Status.second. Also, we’d need to constrain the values of the digit between 0 and 9.

To add such side conditions on the actions of our model, we can define validate_Char class method. The method returns False when the action is invalid and True otherwise:

    def validate_Char(self, op : Op, digit : int):
        if digit < 0 or digit > 9:
            return False
        if op == Op.plus and self.status != Status.first:
            return False
        if op == Op.end and self.status != Status.second:
            return False
        return True

Finally, we need to supply a decomposition scenario. For this, you have to define a global list with the sequence of actions you want for the decomposition. Let’s say we want to see all possible ways our model behaves with at most 7 incoming characters / Char actions. Then we add the following string to our model:

scenario = ['Char','Char','Char','Char','Char','Char', 'Char']

Saving all the model code above into an adder.py file, we can run the decomposition by passing it to the imandra.idf.decompose function. This will start the decomposition job in the cloud and will return a decomposition handle, which can be used to request the job status:

from imandra import idf

with open("adder.py", "r") as f:
    code = f.read() 

decomposition = idf.decompose(code)
decomposition.status()

When decomposition.status() becomes {"status": "done"}, we are ready to retrieve the generated Python code. We can get the Python string with the code by calling decomposition.dumps(). The generated code is usually very long, so let us look at a couple of first lines in it:

for l in decomposition.dumps().splitlines()[:10]:
    print(l)

We can use Python exec to load the whole code in th current Python session:

exec(decomposition.dumps())