# (Generally) How to specify asynchronous action with side effects using logic equations

Say you have this function call sequence:

function all() {
fn1()
fn2()
fn3()
}


And say that fn2 was asynchronous and caused all kinds of side effects:

var globalPacketCounter = 0

function fn2() {
var httpRequest = ...
httpRequest.on('data', function(){
globalPacketCounter++
})
drawGraphicsToDisplay()
...
}


Something complicated and with unknown implementation, though you can probe it to determine the types of behavior it has, and read docs, etc.

I'm wondering, generally speaking, what you can do to incorporate this into a model checking or symbolic evaluation system, or other verification system like Hoare logic or something. I would like to do this:

all() =
/\ fn1() in state 1
/\ fn2() in state 2
/\ fn3() in state 3
/\ complete = true in state 4


Some sort of logical statement. The question is (partially) if this is a valid approach; that is, treating the fn2() as a single step in a logic equation. The main part of the question though is how to generally do this. I would like to basically treat everything as logic functions but am not sure how to apply it to the "async with side effects" case.

One way to model your example is through program graphs. (See chapter 2 in Principles of Model Checking.) What you can do is model all() as one program, which synchronizes on action 'data' with another program that runs concurrently to all(), let's call it listen(). listen() will have an initial state where it waits until it can synchronize with the all() on action 'data'.