Echtzeitsysteme/tchecker
1
0
Fork 0
mirror of https://github.com/Echtzeitsysteme/tchecker.git synced 2024-05-20 20:00:44 +00:00
Code Issues Packages Projects Releases Wiki Activity

chg: add JSON output format

Browse source
This commit is contained in:
Gerald Point 2022-06-27 10:57:42 +02:00
parent 4d0331e29b
commit 199f947be8
4 changed files with 237 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

39
doc/json-spec.md Normal file
View file

@ -0,0 +1,39 @@
```
{
"name" : string,
"processes" : [
{
"pid" : string,
"locations" : [
{
"id" : string
"attributes" : {
"attr" : "value",
...
}
},
...
],
"edges" : [
{
"src" : string,
"tgt" : string,
"attributes" : {
"attr" : "value",
...
}
}
]
},
...
},
"sync" : [
[ "label1", ..., "labeln"],
...
]
}
```

11
include/tchecker/system/output.hh
View file

@ -45,6 +45,17 @@ void output_tck(std::ostream & os, tchecker::system::system_t const & s);
*/
void output_dot(std::ostream & os, tchecker::system::system_t const & s, std::string const & delimiter);
/*!
\brief Output a system following the JSON syntax
\param os : output stream
\param s : system
\param delimiter : separator between process name and location name for node
names
\post s has been output to os following the dot graphviz syntax
\throw std::runtime_error : if a location or an edge in s has an attribute "label"
*/
void output_json(std::ostream & os, tchecker::system::system_t const & s, std::string const & delimiter);
} // end of namespace system
} // end of namespace tchecker

162
src/system/output.cc
View file

@ -189,6 +189,168 @@ void output_dot(std::ostream & os, tchecker::system::system_t const & s, std::st
os << "}" << std::endl;
}
//
// JSON pretty-printer
//
static std::string const json_tab = " ";
static void json_output_attributes(std::ostream & os,
tchecker::system::attributes_t const & attr,
std::string const t0)
{
std::string const t1 = t0+json_tab;
auto r = attr.attributes();
os << t0 << "\"attributes\" : {" << std::endl;
if (r.begin() != r.end()) {
auto begin = r.begin(), end = r.end();
for (auto it = begin; it != end; ++it) {
if (it != begin)
os << "," << std::endl;
os << t1 << "\"" << (*it).first << "\" : \"" << (*it).second << "\"";
}
os << t1 << std::endl;
}
os << t0 << "}" << std::endl;
}
static void json_output_location(std::ostream & os,
tchecker::system::system_t const & s,
std::string const & delimiter,
tchecker::process_id_t pid,
tchecker::system::loc_const_shared_ptr_t & loc,
bool first,
std::string const t0)
{
std::string const t1 = t0+json_tab;
std::string const locid = dot_node_name(s.process_name(loc->pid()), loc->name(), delimiter);
if (! first)
os << "," << std::endl;
os << t0 << "{" << std::endl
<< t1 << "\"id\" : \"" << locid << "\"," << std::endl;
tchecker::system::attributes_t attr{loc->attributes()};
if (!attr.values("label").empty())
throw std::runtime_error("location already has a \"label\" attribute");
attr.add_attribute("label", loc->name());
json_output_attributes(os, attr, t1);
os << t0 << "}";
}
static void json_output_edge(std::ostream & os,
tchecker::system::system_t const & s,
std::string const & delimiter,
tchecker::process_id_t pid,
tchecker::system::edge_const_shared_ptr_t & edge,
bool first,
std::string const t0)
{
std::string t1 = t0+json_tab;
std::string pname = s.process_name(edge->pid());
std::string src_name = s.location(edge->src())->name();
std::string tgt_name = s.location(edge->tgt())->name();
if (!first)
os << "," << std::endl;
os << t0 << "{" << std::endl
<< t1 << "\"src\" : \"" << dot_node_name(pname, src_name, delimiter) << "\"," << std::endl
<< t1 << "\"tgt\" : \"" << dot_node_name(pname, tgt_name, delimiter) << "\"," << std::endl;
tchecker::system::attributes_t attr{edge->attributes()};
if (!attr.values("label").empty())
throw std::runtime_error("edge already has a \"label\" attribute");
attr.add_attribute("label", s.event_name(edge->event_id()));
json_output_attributes(os, attr, t1);
os << t0 << "}"; // end of edge
}
static void json_output_process(std::ostream & os,
tchecker::system::system_t const & s,
std::string const & delimiter,
tchecker::process_id_t pid,
std::string const t0)
{
std::string const t1 = t0+json_tab;
os << t0 << "{" << std::endl
<< t1 << "\"pid\" : \"" << s.process_name(pid) << "\"," << std::endl
<< t1 << "\"locations\" : [" << std::endl;
// Locations
bool first = true;
for (tchecker::system::loc_const_shared_ptr_t loc : s.locations()) {
if (loc->pid() != pid)
continue;
json_output_location(os, s, delimiter, pid, loc, first, t1 + json_tab);
first = false;
}
if (! first)
os << std::endl;
os << t1 << "]," << std::endl; // end of locations
os<< t1 << "\"edges\" : [" << std::endl;
first = true;
for (tchecker::system::edge_const_shared_ptr_t edge : s.edges()) {
if (edge->pid() != pid)
continue;
json_output_edge(os, s, delimiter, pid, edge, first, t1 + json_tab);
first = false;
}
if (! first)
os << std::endl;
os << t1 << "]" << std::endl; //end of edges
os << t0 << "}"; // end of process
}
static void json_output_sync(std::ostream & os,
tchecker::system::synchronization_t const & sync,
tchecker::system::system_t const & s,
std::string const t0,
bool first)
{
std::string const t1 = t0+json_tab;
if (!first)
os << "," << std::endl;
os << t1 << "[ ";
auto r = sync.synchronization_constraints();
for (auto it = r.begin(); it != r.end(); ++it) {
if (it != r.begin())
os << ", ";
tchecker::system::sync_constraint_t const & constr = *it;
os << "\"" << s.process_name(constr.pid()) << "@" << s.event_name(constr.event_id());
if (constr.strength() == tchecker::SYNC_WEAK)
os << "?";
os << "\"";
}
os << " ]";
}
void output_json(std::ostream & os, tchecker::system::system_t const & s, std::string const & delimiter)
{
std::string const t1 = json_tab;
os << "{" << std::endl
<< t1 << "\"name\" : \"" << s.name() << "\"," << std::endl
<< t1 << "\"processes\" : [" << std::endl;
tchecker::process_id_t processes_count = s.processes_count();
for (tchecker::process_id_t pid = 0; pid < processes_count; ++pid) {
json_output_process(os, s, delimiter, pid, t1 + json_tab);
if (pid + 1 < processes_count)
os << ",";
os << std::endl;
}
os << t1 << "]," << std::endl
<< t1 << "\"sync\" : [" << std::endl;
bool first = true;
for (tchecker::system::synchronization_t const & sync : s.synchronizations()) {
json_output_sync(os, sync, s, t1 + json_tab, first);
first = false;
}
if (! first)
os << std::endl;
os << t1 << "]" << std::endl
<< "}" << std::endl;
}
} // end of namespace system
} // end of namespace tchecker

26
src/tck-syntax/tck-syntax.cc
View file

@ -32,10 +32,11 @@ static struct option long_options[] = {{"check", no_argument, 0, 'c'},
{"delimiter", required_argument, 0, 'd'},
{"process-name", required_argument, 0, 'n'},
{"transform", no_argument, 0, 't'},
{"json", no_argument, 0, 'j'},
{"help", no_argument, 0, 'h'},
{0, 0, 0, 0}};
static char * const options = (char *)"cd:hn:o:pt";
static char * const options = (char *)"cd:hn:o:ptj";
void usage(char * progname)
{
@ -43,6 +44,7 @@ void usage(char * progname)
std::cerr << " -c syntax check (timed automaton)" << std::endl;
std::cerr << " -p synchronized product" << std::endl;
std::cerr << " -t transform a system into dot graphviz file format" << std::endl;
std::cerr << " -j transform a system into json file format" << std::endl;
std::cerr << " -o file output file" << std::endl;
std::cerr << " -d delim delimiter string (default: _)" << std::endl;
std::cerr << " -n name name of synchronized process (default: P)" << std::endl;
@ -53,6 +55,7 @@ void usage(char * progname)
static bool check_syntax = false;
static bool synchronized_product = false;
static bool transform = false;
static bool json = false;
static bool help = false;
static std::string delimiter = "_";
static std::string process_name = "P";
@ -95,6 +98,9 @@ int parse_command_line(int argc, char * argv[])
case 't':
transform = true;
break;
case 'j':
json = true;
break;
default:
throw std::runtime_error("I should never be executed");
break;
@ -172,6 +178,22 @@ void do_output_dot(tchecker::parsing::system_declaration_t const & sysdecl, std:
os << std::endl;
}
/*!
\brief Output a system of processes following the JSON format
\param sysdecl : system declaration
\param delimiter : delimiter used in node names
\param os : output stream
\post The system of processes in sysdecl has been output to os following the
JSON format, using delimiter as a separator between process name and
location name for node names.
*/
void do_output_json(tchecker::parsing::system_declaration_t const & sysdecl, std::string const & delimiter, std::ostream & os)
{
std::shared_ptr<tchecker::system::system_t> system(new tchecker::system::system_t(sysdecl));
tchecker::system::output_json(os, *system, delimiter);
os << std::endl;
}
/*!
\brief Main function
*/
@ -218,6 +240,8 @@ int main(int argc, char * argv[])
if (transform)
do_output_dot(*sysdecl, delimiter, *os);
else if (json)
do_output_json(*sysdecl, delimiter, *os);
}
catch (std::exception & e) {
std::cerr << tchecker::log_error << e.what() << std::endl;