# How to Construct Kripke Structure States from Nested Functions

Say I have these defined functions:

function a(x, y, z){
var q = b(y)
q = c(q, z, x)
q = d(q)
return q
}

function b(x) {
var q = e(x)
q = f(q)
return q
}

function c(x, y, z) {
return x + y * z
}

function d(x) {
return x * 10
}

function e(x) {
return x + 5
}

function f(x) {
return x - 3
}


I want to then create a model for model checking. It needs a set of states. I'm wondering what those states look like, and what the scope of them is. That is, the questions are:

1. If the states are defined per function definition, per function application, or both.
2. If the function applications need to be "expanded" to the lowest-level function (to "atomic statements" or "atomic functions").
3. What the transitive closure looks like for a particular pair of states (the transition relation) (if I did it right, below).
4. What becomes a BDD, wondering if it just the "states" below, or the "transition relation" as well, or the transition relation between all states in the reachability graph, or more.

From my understanding so far, I create a Kripke Structure for this program first. This gives me the states. This is the crux of what I'm wondering. So first attempt, each function invocation will have it's own state. I start off like this:

var x = 1
var y = 2
var z = 3
// initial state == { x == 1, y == 2, z == 3 }
x = a(x, y, z)
// final state == { x == integer, y == 2, z == 3}


I am not sure if I would then encode this function invocation's state as $x = 1 \land y = 2 \land z = 3$, and how to scope it to the current function.

Anyways, if I were to expand this function, it would become:

var q = b(y)
q = c(q, z, x)
q = d(q)


...

var q = e(y)
q = f(q)
q = q + z * x
q = q * 10


...

var q = y + 5
q = q - 3
q = q + z * x
q = q * 10


Wondering if this is supposed to be done. This would mean there are a set of global variables. The states are then defined between the statements using the global variables.

// state = { x == 1, y == 2, z == 3, q == null }
var q = y + 5
// state = { x == 1, y == 2, z == 3, q == 7 }
q = q - 3
// state = { x == 1, y == 2, z == 3, q == 4 }
q = q + z * x
// state = { x == 1, y == 2, z == 3, q == 7 }
q = q * 10
// state = { x == 1, y == 2, z == 3, q == 70 }
x = q
// state = { x == 70, y == 2, z == 3, q == 70 }


Each of these states should then be converted into a BDD (Binary Decision Diagram) (correct me if I'm wrong).

Wondering if there is a way to do this without "expanding" the function like this so variables become global, and instead do it using locally scoped variables based on their original function definition somehow.

Then the reachable state is the set of states reachable from a given state. So all the states are reachable from the first state:

// from
//    state = { x == 1, y == 2, z == 3, q == null }
// to
//    state = { x == 1, y == 2, z == 3, q == 7 }
//    state = { x == 1, y == 2, z == 3, q == 4 }
//    state = { x == 1, y == 2, z == 3, q == 7 }
//    state = { x == 1, y == 2, z == 3, q == 70 }
//    state = { x == 70, y == 2, z == 3, q == 70 }


Not sure if I am then supposed to create a transition relation between each state, so it would create a sort of boolean logic expression, which could then be matched with a temporal logic expression from a specification, e.g.:

// transition from the first to the last state
//    { x == 1, y == 2, z == 3, q == null, x': 70, y': 2, z': 3, q': 70 }


Then this "transition relation" becomes a BDD. The model checker then uses these transitions as well as the plain states to check against the specification somehow.

Please let me know if I'm on the right track. The questions are those listed questions above. Thank you so much for your time.

(1) The model checker starts in an initial pristine state (an empty, formatted disk) and recursively generates and checks successive states by systematically executing state transitions. Transitions are either test driver operations or FS-specific kernel threads which flush blocks to disk. The test driver is conceptually similar to a program run during testing. It creates, removes, and renames files, directories, and hard links; writes to and truncates files; and mounts and unmounts the file system.