Syft::GR1 Struct Reference

#include <GR1.h>

Static Public Member Functions
static CUDD::BDD	read_gr1_justice (const std::shared_ptr< VarMgr > &var_mgr, std::istream &in, std::size_t &line_number)
	Stores a player justice.
static std::runtime_error	bad_file_format_exception (std::size_t line_number)
static GR1	read_from_gr1_file (const std::shared_ptr< VarMgr > &var_mgr, const std::string &gr1_filename)
	Stores a GR(1) condition. More...

Public Attributes
std::vector< CUDD::BDD >	env_justices
std::vector< CUDD::BDD >	agn_justices

Detailed Description

GR(1) file format is similar to the regular CNF format, such that every justice is represented as a conjunction over disjunctive clauses. Each justice is labeled with env or agn to refer to environment or agent justice respectively, and ended with end. Consider GR(1) formula GF(p_1) & GF(p_1 & q_1) & ... & GF(!p_1 & (q_1 | q_2)) -> GF(q_1) & GF(p_1 & q_1) & ... & GF(!q_1 & (p_1 | p_2)), this formula is written as follows (variables in uppercase): –Env-Justice– P_1 –Justice-End–

–Env-Justice– P_1 Q_1 –Justice-End–

–Env-Justice– !P_1 Q_1 Q_2 –Justice-End–

–Agn-Justice– Q_1 –Justice-End–

–Agn-Justice– P_1 Q_1 –Justice-End–

–Agn-Justice– !Q_1 P_1 Q_1 –Justice-End– End

Member Function Documentation

read_from_gr1_file()

static GR1 Syft::GR1::read_from_gr1_file ( const std::shared_ptr< VarMgr > &  var_mgr, const std::string &  gr1_filename  )

inlinestatic

Stores a GR(1) condition.

Parameters

gr1_filename

The name of the file to read the GR(1) condition from.

Returns

The GR(1) condition stored in the file

---

The documentation for this struct was generated from the following file:

• src/synthesis/header/GR1.h