!rm -f test1.dve

%%file test1.dve
int a = 0, b = 0;

process P {
 state x;
 init x;

 trans
   x -> x { guard a < 3 && b < 3; effect a = a + 1; },
   x -> x { guard a < 3 && b < 3; effect b = b + 1; };
}

process Q {
  state wait, work;
  init wait;
  trans
    wait -> work { guard b > 1; },
    work -> wait { guard a > 1; };
}

system async;

"""
Explanation: There are two ways to load a DiVinE model: from a file or from a cell.   
Loading from a file
We will first start with the file version, however because this notebook should also be a self-contained test case, we start by writing a model into a file.
End of explanation
"""


m = spot.ltsmin.load('test1.dve')

"""
Explanation: The spot.ltsmin.load function compiles the model using the ltlmin interface and load it.  This should work with DiVinE models if divine --LTSmin works, and with Promela models if spins is installed.
End of explanation
"""


!rm -f test1.dve test1.dve.cpp test1.dve2C

"""
Explanation: Compiling the model creates all several kinds of files.  The test1.dve file is converted into a C++ source code test1.dve.cpp which is then compiled into a shared library test1.dve2c.  Becauce spot.ltsmin.load() has already loaded this shared library, all those files can be erased.  If you do not erase the files, spot.ltsmin.load() will use the timestamps to decide whether the library should be recompiled or not everytime you load the library.
For editing and loading DVE file from a notebook, it is a better to use the %%dve as shown next.
End of explanation
"""


%%dve m
int a = 0, b = 0;

process P {
 state x;
 init x;

 trans
   x -> x { guard a < 3 && b < 3; effect a = a + 1; },
   x -> x { guard a < 3 && b < 3; effect b = b + 1; };
}

process Q {
  state wait, work;
  init wait;
  trans
    wait -> work { guard b > 1; },
    work -> wait { guard a > 1; };
}

system async;

"""
Explanation: Loading from a notebook cell
The %%dve cell magic implements all of the above steps (saving the model into a temporary file, compiling it, loading it, erasing the temporary files).  The variable name that should receive the model (here m) should be indicated on the first line, after %dve.
End of explanation
"""


m

sorted(m.info().items())

"""
Explanation: Working with an ltsmin model
Printing an ltsmin model shows some information about the variables it contains and their types, however the info() methods provide the data in a map that is easier to work with.
End of explanation
"""


k = m.kripke(["a<1", "b>2"])
k

k.show('.<15')

k.show('.<0')  # unlimited output

a = spot.translate('"a<1" U "b>2"'); a

spot.otf_product(k, a)

"""
Explanation: To obtain a Kripke structure, call kripke and supply a list of atomic propositions to observe in the model.
End of explanation
"""


a = spot.atomic_prop_collect(spot.formula('"a < 2" W "b == 1"')); a

def model_check(f, m):
    f = spot.formula(f)
    ss = m.kripke(spot.atomic_prop_collect(f))
    nf = spot.formula_Not(f).translate()
    return spot.otf_product(ss, nf).is_empty() 

model_check('"a<1" R "b > 1"', m)

"""
Explanation: If we want to create a model_check function that takes a model and formula, we need to get the list of atomic propositions used in the formula using atomic_prop_collect().  This returns an atomic_prop_set:
End of explanation
"""


def model_debug(f, m):
    f = spot.formula(f)
    ss = m.kripke(spot.atomic_prop_collect(f))
    nf = spot.formula_Not(f).translate()
    return ss.intersecting_run(nf)

run = model_debug('"a<1" R "b > 1"', m); run

"""
Explanation: Instead of otf_product(x, y).is_empty() we prefer to call !x.intersects(y).  There is also x.intersecting_run(y) that can be used to return a counterexample.
End of explanation
"""


run.as_twa(True)

"""
Explanation: This accepting run can be represented as an automaton (the True argument requires the state names to be preserved).  This can be more readable.
End of explanation
"""


