-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
0 parents
commit fe27aad
Showing
599 changed files
with
33,526 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,133 @@ | ||
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "https://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> | ||
<html xmlns="http://www.w3.org/1999/xhtml"> | ||
<head> | ||
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/> | ||
<meta http-equiv="X-UA-Compatible" content="IE=9"/> | ||
<meta name="generator" content="Doxygen 1.9.1"/> | ||
<meta name="viewport" content="width=device-width, initial-scale=1"/> | ||
<title>LydiaSyft: src/synthesis/header/game/BuchiReachability.hpp Source File</title> | ||
<link href="tabs.css" rel="stylesheet" type="text/css"/> | ||
<script type="text/javascript" src="jquery.js"></script> | ||
<script type="text/javascript" src="dynsections.js"></script> | ||
<link href="navtree.css" rel="stylesheet" type="text/css"/> | ||
<script type="text/javascript" src="resize.js"></script> | ||
<script type="text/javascript" src="navtreedata.js"></script> | ||
<script type="text/javascript" src="navtree.js"></script> | ||
<link href="search/search.css" rel="stylesheet" type="text/css"/> | ||
<script type="text/javascript" src="search/searchdata.js"></script> | ||
<script type="text/javascript" src="search/search.js"></script> | ||
<link href="doxygen.css" rel="stylesheet" type="text/css" /> | ||
</head> | ||
<body> | ||
<div id="top"><!-- do not remove this div, it is closed by doxygen! --> | ||
<div id="titlearea"> | ||
<table cellspacing="0" cellpadding="0"> | ||
<tbody> | ||
<tr style="height: 56px;"> | ||
<td id="projectalign" style="padding-left: 0.5em;"> | ||
<div id="projectname">LydiaSyft | ||
</div> | ||
</td> | ||
</tr> | ||
</tbody> | ||
</table> | ||
</div> | ||
<!-- end header part --> | ||
<!-- Generated by Doxygen 1.9.1 --> | ||
<script type="text/javascript"> | ||
/* @license magnet:?xt=urn:btih:cf05388f2679ee054f2beb29a391d25f4e673ac3&dn=gpl-2.0.txt GPL-v2 */ | ||
var searchBox = new SearchBox("searchBox", "search",false,'Search','.html'); | ||
/* @license-end */ | ||
</script> | ||
<script type="text/javascript" src="menudata.js"></script> | ||
<script type="text/javascript" src="menu.js"></script> | ||
<script type="text/javascript"> | ||
/* @license magnet:?xt=urn:btih:cf05388f2679ee054f2beb29a391d25f4e673ac3&dn=gpl-2.0.txt GPL-v2 */ | ||
$(function() { | ||
initMenu('',true,false,'search.php','Search'); | ||
$(document).ready(function() { init_search(); }); | ||
}); | ||
/* @license-end */</script> | ||
<div id="main-nav"></div> | ||
</div><!-- top --> | ||
<div id="side-nav" class="ui-resizable side-nav-resizable"> | ||
<div id="nav-tree"> | ||
<div id="nav-tree-contents"> | ||
<div id="nav-sync" class="sync"></div> | ||
</div> | ||
</div> | ||
<div id="splitbar" style="-moz-user-select:none;" | ||
class="ui-resizable-handle"> | ||
</div> | ||
</div> | ||
<script type="text/javascript"> | ||
/* @license magnet:?xt=urn:btih:cf05388f2679ee054f2beb29a391d25f4e673ac3&dn=gpl-2.0.txt GPL-v2 */ | ||
$(document).ready(function(){initNavTree('BuchiReachability_8hpp_source.html',''); initResizable(); }); | ||
/* @license-end */ | ||
</script> | ||
<div id="doc-content"> | ||
<!-- window showing the filter options --> | ||
<div id="MSearchSelectWindow" | ||
onmouseover="return searchBox.OnSearchSelectShow()" | ||
onmouseout="return searchBox.OnSearchSelectHide()" | ||
onkeydown="return searchBox.OnSearchSelectKey(event)"> | ||
</div> | ||
|
||
<!-- iframe showing the search results (closed by default) --> | ||
<div id="MSearchResultsWindow"> | ||
<iframe src="javascript:void(0)" frameborder="0" | ||
name="MSearchResults" id="MSearchResults"> | ||
</iframe> | ||
</div> | ||
|
||
<div class="header"> | ||
<div class="headertitle"> | ||
<div class="title">BuchiReachability.hpp</div> </div> | ||
</div><!--header--> | ||
<div class="contents"> | ||
<div class="fragment"><div class="line"><a name="l00001"></a><span class="lineno"> 1</span> <span class="comment">//</span></div> | ||
<div class="line"><a name="l00002"></a><span class="lineno"> 2</span> <span class="comment">// Created by shuzhu on 16/04/24.</span></div> | ||
<div class="line"><a name="l00003"></a><span class="lineno"> 3</span> <span class="comment">//</span></div> | ||
<div class="line"><a name="l00004"></a><span class="lineno"> 4</span>  </div> | ||
<div class="line"><a name="l00005"></a><span class="lineno"> 5</span> <span class="preprocessor">#ifndef LYDIASYFT_BUCHIREACHABILITY_HPP</span></div> | ||
<div class="line"><a name="l00006"></a><span class="lineno"> 6</span> <span class="preprocessor">#define LYDIASYFT_BUCHIREACHABILITY_HPP</span></div> | ||
<div class="line"><a name="l00007"></a><span class="lineno"> 7</span>  </div> | ||
<div class="line"><a name="l00008"></a><span class="lineno"> 8</span> <span class="preprocessor">#include "game/DfaGameSynthesizer.h"</span></div> | ||
<div class="line"><a name="l00009"></a><span class="lineno"> 9</span>  </div> | ||
<div class="line"><a name="l00010"></a><span class="lineno"> 10</span> <span class="keyword">namespace </span>Syft {</div> | ||
<div class="line"><a name="l00016"></a><span class="lineno"><a class="line" href="classSyft_1_1BuchiReachability.html"> 16</a></span>  <span class="keyword">class </span><a class="code" href="classSyft_1_1BuchiReachability.html">BuchiReachability</a> : <span class="keyword">public</span> <a class="code" href="classSyft_1_1DfaGameSynthesizer.html">DfaGameSynthesizer</a> {</div> | ||
<div class="line"><a name="l00017"></a><span class="lineno"> 17</span>  <span class="keyword">private</span>:</div> | ||
<div class="line"><a name="l00021"></a><span class="lineno"> 21</span>  CUDD::BDD goal_states_;</div> | ||
<div class="line"><a name="l00025"></a><span class="lineno"> 25</span>  CUDD::BDD state_space_;</div> | ||
<div class="line"><a name="l00029"></a><span class="lineno"> 29</span>  CUDD::BDD Buchi_;</div> | ||
<div class="line"><a name="l00030"></a><span class="lineno"> 30</span>  </div> | ||
<div class="line"><a name="l00031"></a><span class="lineno"> 31</span>  <span class="keyword">public</span>:</div> | ||
<div class="line"><a name="l00032"></a><span class="lineno"> 32</span>  </div> | ||
<div class="line"><a name="l00043"></a><span class="lineno"> 43</span>  <a class="code" href="classSyft_1_1BuchiReachability.html#abc9591a945c0bbe104d027bce1de07b5">BuchiReachability</a>(<span class="keyword">const</span> <a class="code" href="classSyft_1_1SymbolicStateDfa.html">SymbolicStateDfa</a> &spec, Player starting_player, Player protagonist_player,</div> | ||
<div class="line"><a name="l00044"></a><span class="lineno"> 44</span>  <span class="keyword">const</span> CUDD::BDD &goal_states, <span class="keyword">const</span> CUDD::BDD &Buchi, <span class="keyword">const</span> CUDD::BDD &state_space);</div> | ||
<div class="line"><a name="l00045"></a><span class="lineno"> 45</span>  </div> | ||
<div class="line"><a name="l00046"></a><span class="lineno"> 46</span>  </div> | ||
<div class="line"><a name="l00055"></a><span class="lineno"> 55</span>  <a class="code" href="structSyft_1_1SynthesisResult.html">SynthesisResult</a> <a class="code" href="classSyft_1_1BuchiReachability.html#a9f1945cbb20abdd0bff1f0606ca352d4">run</a>() <span class="keyword">const</span> <span class="keyword">final</span>;</div> | ||
<div class="line"><a name="l00056"></a><span class="lineno"> 56</span>  </div> | ||
<div class="line"><a name="l00057"></a><span class="lineno"> 57</span>  };</div> | ||
<div class="line"><a name="l00058"></a><span class="lineno"> 58</span> }</div> | ||
<div class="line"><a name="l00059"></a><span class="lineno"> 59</span>  </div> | ||
<div class="line"><a name="l00060"></a><span class="lineno"> 60</span>  </div> | ||
<div class="line"><a name="l00061"></a><span class="lineno"> 61</span> <span class="preprocessor">#endif </span><span class="comment">//LYDIASYFT_BUCHIREACHABILITY_HPP</span></div> | ||
<div class="ttc" id="aclassSyft_1_1BuchiReachability_html"><div class="ttname"><a href="classSyft_1_1BuchiReachability.html">Syft::BuchiReachability</a></div><div class="ttdoc">A single-strategy-synthesizer for a Buchi-reachability game given as a symbolic-state DFA.</div><div class="ttdef"><b>Definition:</b> BuchiReachability.hpp:16</div></div> | ||
<div class="ttc" id="aclassSyft_1_1BuchiReachability_html_a9f1945cbb20abdd0bff1f0606ca352d4"><div class="ttname"><a href="classSyft_1_1BuchiReachability.html#a9f1945cbb20abdd0bff1f0606ca352d4">Syft::BuchiReachability::run</a></div><div class="ttdeci">SynthesisResult run() const final</div><div class="ttdoc">Solves the Buchi-reachability game.</div><div class="ttdef"><b>Definition:</b> BuchiReachability.cpp:17</div></div> | ||
<div class="ttc" id="aclassSyft_1_1BuchiReachability_html_abc9591a945c0bbe104d027bce1de07b5"><div class="ttname"><a href="classSyft_1_1BuchiReachability.html#abc9591a945c0bbe104d027bce1de07b5">Syft::BuchiReachability::BuchiReachability</a></div><div class="ttdeci">BuchiReachability(const SymbolicStateDfa &spec, Player starting_player, Player protagonist_player, const CUDD::BDD &goal_states, const CUDD::BDD &Buchi, const CUDD::BDD &state_space)</div><div class="ttdoc">Construct a single-strategy-synthesizer for the given Buchi-reachability game.</div><div class="ttdef"><b>Definition:</b> BuchiReachability.cpp:8</div></div> | ||
<div class="ttc" id="aclassSyft_1_1DfaGameSynthesizer_html"><div class="ttname"><a href="classSyft_1_1DfaGameSynthesizer.html">Syft::DfaGameSynthesizer</a></div><div class="ttdoc">A synthesizer for a game whose arena is a symbolic-state DFA.</div><div class="ttdef"><b>Definition:</b> DfaGameSynthesizer.h:15</div></div> | ||
<div class="ttc" id="aclassSyft_1_1SymbolicStateDfa_html"><div class="ttname"><a href="classSyft_1_1SymbolicStateDfa.html">Syft::SymbolicStateDfa</a></div><div class="ttdoc">A DFA with symbolic states and transitions.</div><div class="ttdef"><b>Definition:</b> SymbolicStateDfa.h:18</div></div> | ||
<div class="ttc" id="astructSyft_1_1SynthesisResult_html"><div class="ttname"><a href="structSyft_1_1SynthesisResult.html">Syft::SynthesisResult</a></div><div class="ttdef"><b>Definition:</b> Synthesizer.h:16</div></div> | ||
</div><!-- fragment --></div><!-- contents --> | ||
</div><!-- doc-content --> | ||
<!-- start footer part --> | ||
<div id="nav-path" class="navpath"><!-- id is needed for treeview function! --> | ||
<ul> | ||
<li class="navelem"><a class="el" href="dir_68267d1309a1af8e8297ef4c3efbcdba.html">src</a></li><li class="navelem"><a class="el" href="dir_957d8196b17c2a3ea74332cb4b59d36d.html">synthesis</a></li><li class="navelem"><a class="el" href="dir_d46d0e22f608a1c36cc907cacfa408f6.html">header</a></li><li class="navelem"><a class="el" href="dir_5b99d129890bb6c8686fe210e25999ea.html">game</a></li><li class="navelem"><b>BuchiReachability.hpp</b></li> | ||
<li class="footer">Generated by <a href="https://www.doxygen.org/index.html"><img class="footer" src="doxygen.svg" width="104" height="31" alt="doxygen"/></a> 1.9.1 </li> | ||
</ul> | ||
</div> | ||
</body> | ||
</html> |
Oops, something went wrong.