====== Overview ====== A large number of models that are employed in the field of concurrent systems design, such as [[wp>Petri_net|Petri nets]], [[wp>Asynchronous_circuit|gate-level circuits]], [[wp>Data_flow_diagram|dataflow structures]], etc. - all have an underlying static [[wp>Graph_(mathematics)|graph]] structure. Their semantics, however, is defined using additional entities, e.g. tokens or node/arc states, which in turn form the overall state of the system. We jointly refer to such formalisms as //interpreted graph models//. The similarities between the interpreted graph models allow for links between different formalisms to be created, either by means of adapter interfaces or by conversion from one model type into another. This greatly extends the range of applicable modelling and analysis techniques. Workcraft is designed to provide a flexible common framework for development of interpreted graph models, including visual editing, (co)simulation and analysis. The latter can be carried out either directly or by mapping a model into a behaviourally equivalent model of a different type (usually a Petri net). Hence the user can design a system using the most appropriate formalism (or even different formalisms for the subsystems), while still utilising the power of Petri net analysis techniques. Below is a summary of the currently supported interpreted graph models that are implemented as as plug-ins for Workcraft framework. ^ Model ^ Supported features ^^^^ ^ ::: ^ Editing ^ Simulation ^ Verification ^ Synthesis ^ | **abstract behaviour** ||||| ^ [[graph|Directed Graph]]\ [(dg_wiki)]%% %%| @#AAFFAA:Yes | @#AAFFAA:Yes | @#AAFFAA:Yes | @#FFFFFF:n/a | ^ [[fsm|Finite State Machine]]\ [(fsm_wiki)]%% %%| @#AAFFAA:Yes | @#AAFFAA:Yes | @#AAFFAA:Yes | @#AAFFAA:Yes((synthesis into Petri Net)) | ^ [[petri|Petri Net]]\ [(pn_wiki)]%% %%| @#AAFFAA:Yes | @#AAFFAA:Yes | @#AAFFAA:Yes | @#AAFFAA:Yes((re-synthesis into simpler Petri Net)) | ^ [[policy|Policy Net]] [(Fernandes_2013_atpn)]%% %%| @#AAFFAA:Yes | @#AAFFAA:Yes | @#AAFFAA:Yes | @#AAFFAA:Yes((synthesis into Petri Net)) | | **signal semantics** ||||| ^ [[dtd|Digital Timing Diagram]]\ [(dtd_wiki)]%% %%| @#AAFFAA:Yes | @#FFAAAA:No | @#FFAAAA:No | @#FFFFFF:n/a | ^ [[wtg|Waveform Transition Graph]]\ [(Cortadella_2017_async)]%% %%| @#AAFFAA:Yes | @#AAFFAA:Yes | @#FFFFAA:Some | @#AAFFAA:Yes((via translation to synthesisable Signal Transition Graph)) | ^ [[fst|Finite State Transducer]]\ [(fst_wiki)]%% %%| @#AAFFAA:Yes | @#AAFFAA:Yes | @#AAFFAA:Yes | @#AAFFAA:Yes((into Signal Transition Graph)) | ^ [[stg|Signal Transition Graph]]\ [(Yakovlev_1996_fmsd)]%% %%| @#AAFFAA:Yes | @#AAFFAA:Yes | @#AAFFAA:Yes | @#AAFFAA:Yes((synthesis into Digital Circuit and re-synthesis into simpler Petri Net)) | ^ [[cpog|Conditional Partial Order Graph]]\ [(Mokhov_2010_ieeetc)]%% %%| @#AAFFAA:Yes | @#FFFFAA:Some | @#FFAAAA:No | @#AAFFAA:Yes((synthesis into Digital Circuit)) | | **structural information** ||||| ^ [[son|Structured Occurrence Net]]\ [(Koutny_2009_fi)]%% %%| @#AAFFAA:Yes | @#AAFFAA:Yes | @#AAFFAA:Yes | @#FFFFFF:n/a | ^ [[dfs|Dataflow Structure]]\ [(Sokolov_2008_fi)]%% %%| @#AAFFAA:Yes | @#AAFFAA:Yes | @#AAFFAA:Yes | @#FFAAAA:No | ^ [[circuit|Digital Circuit]]\ [(Poliakov_2008_async)]%% %%| @#AAFFAA:Yes | @#AAFFAA:Yes | @#AAFFAA:Yes | @#FFFFFF:n/a | ^ [[xmas|xMAS Circuit]]\ [(Chatterjee_2010_hldvt)]%% %%| @#AAFFAA:Yes | @#AAFFAA:Yes | @#FFFFAA:Some | @#FFAAAA:No | {{ model_relationship.svg?nolink |}} [(dg_wiki> [[wp>Directed_graph|Directed Graph]].)] [(fsm_wiki> [[wp>Finite-state_machine|Finite State Machine]].)] [(pn_wiki> [[wp>Petri_net|Petri net]].)] [(Fernandes_2013_atpn> J.\ Fernandes, M.\ Koutny, M.\ Pietkiewicz-Koutny, D.\ Sokolov, A.\ Yakovlev: //"Step persistence in the design of GALS systems"//, Proc. International Conference on Application and Theory of Petri Nets\ (ATPN), pp.\ 190--209, 2013.)] [(Koutny_2009_fi> M.\ Koutny, B.\ Randell: //"Structured occurrence nets: a formalism for aiding system failure prevention and analysis techniques"//, Fundamenta Informaticae, vol.\ 97(1--2), pp.\ 41--91, 2009.)] [(dtd_wiki> [[wp>Digital_timing_diagram|Digital Timing Diagram]].)] [(Cortadella_2017_async> J.\ Cortadella, A.\ Moreno, D.\ Sokolov, A.\ Yakovlev, D.\ Lloyd: //"Waveform transition graphs: A designer-friendly formalism for asynchronous behaviours"//, Proc. IEEE International Symposium on Asynchronous Circuits and Systems\ (ASYNC), 2017.)] [(fst_wiki> [[wp>Finite_state_transducer|Finite State Transducer]].)] [(Yakovlev_1996_fmsd> A.\ Yakovlev, L.\ Lavagno, A.\ Sangiovanni-Vincentelli: //“A unified signal transition graph model for asynchronous control circuit synthesis”//, Formal Methods in System Design, vol.\ 9(3), pp.\ 139--188, 1996.)] [(Mokhov_2010_ieeetc> A.\ Mokhov, A.\ Yakovlev: //“Conditional partial order graphs: model, synthesis and application”//, IEEE Transactions on Computers, vol.\ 59(11), pp.\ 1480--1493, 2010.)] [(Poliakov_2008_async> I.\ Poliakov, A.\ Mokhov, A.\ Rafiev, D.\ Sokolov, A.\ Yakovlev: //“Automated verification of asynchronous circuits using circuit Petri nets”//, Proc. IEEE International Symposium on Asynchronous Circuits and Systems\ (ASYNC), pp.\ 161--170, 2008.)] [(Sokolov_2008_fi> D.\ Sokolov, I.\ Poliakov, A.\ Yakovlev: //“Analysis of static data flow structures”//, Fundamenta Informaticae, vol. 88(4), pp.\ 581--610, 2008.)] [(Chatterjee_2010_hldvt> S.\ Chatterjee, M.\ Kishinevsky, U.\ Ogras: //"Quick formal modeling of communication fabrics to enable verification"//, Proc. IEEE International Workshop on High Level Design Validation and Test\ (HLDVT), pp.\ 42--49, 2010.)]