json output

[johnyf]

Add output of explicit strategies to the json format described here, because writing a custom parser (or one based on a parser generator) for the jtlv output format everywhere that a strategy needs to be loaded can be avoided. Otherwise, importing an existing parser is tempting, leading to unnecessary dependencies.

If in python the stdout of slugs is stored in variable out, then constructing a networkx graph from the json output is simple and succinct:

import json
import networkx as nx

dout = json.loads(out)
 g = nx.DiGraph()
    dvars = dout['variables']
    for stru, d in dout['nodes'].iteritems():
        u = int(stru)
        state = {k: v for k, v in zip(dvars, d['state'])}
        g.add_node(u, state=state)
        for v in d['trans']:
            g.add_edge(u, v)

The only thing that is missing is a command line option to switch between json and jtlv, for backwards compatibility. Preprocessor conditionals have been used for now in extensions/ExtractExplicitStrategy.hpp, because I am not sure what is the best way to add the argument to the existing mechanism of parsing arguments.

Also, the extensions have been relocated in their own directory, to emphasize what the core sources are, and make it easier to navigate them.

[progirep]

Hi johnyf, I will integrate your change request by modifying the current version of the explicit-state strategy writer -- the most clean way is to add a template parameter, so that every compiled of slugs version includes both the json output and the non-json output.

[progirep]

Hi johnyf, you will see that the latest version of slugs includes json output for explicit strategies. This is basically copy&paste from your pull request, with minor modifications to allow json output to be turned on (and off) without recompiling. There is a new parameter "--jsonOutput" that you can supply to slugs. Thanks a lot for your contribution! I am closing this pull request as the functionality has been added.

[johnyf]

Thank you, @progirep, for implementing the new option for json output.