the (j)torx state-space exploration interface allows on-demand exploration of the state space.
it works like the open/caesar interface of CADP, but then using (textual) commands over a data-stream connection
(stdin/stdout, pipe, tcp connection)
the principle is explained in http://fmt.cs.utwente.nl/tools/torx/torx-explorer.5.html
a slightly extended version is implemented in LTSmin - there the transition identifiers are not used,
but instead always the 'identical state' field is filled with the state identifier of the state reached by a transition.
I should have Java code for the the 'protocol at the 'server' side (where the state space is constructed).
what is needed is mainly:
- identifiers for states that can be passed from 'server' to client and which the client can pass back to refer to a state it has seen before
- a function 'init' that can be called to obtain the identifier of the initial state
- a function 'succ' that can be called with a state identifier as argument, and returns a list (or iterator or whatever) of the outgoing transitions of the state,
with for each transition the label and the identifier of the state reached by the transition
the (j)torx state-space exploration interface allows on-demand exploration of the state space. it works like the open/caesar interface of CADP, but then using (textual) commands over a data-stream connection (stdin/stdout, pipe, tcp connection)
the principle is explained in http://fmt.cs.utwente.nl/tools/torx/torx-explorer.5.html a slightly extended version is implemented in LTSmin - there the transition identifiers are not used, but instead always the 'identical state' field is filled with the state identifier of the state reached by a transition.
I should have Java code for the the 'protocol at the 'server' side (where the state space is constructed).
what is needed is mainly: - identifiers for states that can be passed from 'server' to client and which the client can pass back to refer to a state it has seen before - a function 'init' that can be called to obtain the identifier of the initial state - a function 'succ' that can be called with a state identifier as argument, and returns a list (or iterator or whatever) of the outgoing transitions of the state, with for each transition the label and the identifier of the state reached by the transition
Reported by: axelbel