-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathAPI.html
More file actions
91 lines (64 loc) · 5.15 KB
/
API.html
File metadata and controls
91 lines (64 loc) · 5.15 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
<!DOCTYPE html>
<html lang="en-us">
<head>
<meta charset="UTF-8">
<title></title>
<meta name="description" content=""/>
<meta name="viewport" content="width=device-width, initial-scale=1">
<meta name="theme-color" content="#157878">
<link href='https://fonts.googleapis.com/css?family=Open+Sans:400,700' rel='stylesheet' type='text/css'>
<link rel="stylesheet" href="/temporalTest/assets/css/style.css?v=e6385aa5d099879fe352412a0d0eca6a66f2d907">
</head>
<body>
<section class="page-header">
</section>
<section class="main-content">
<h1 id="API">API Documentation</h1>
<p><font size="4">We explain the main APIs used in writing the specification and configuring <b>RGSE</b>.</p>
<hr />
<h2 id="Symbolic"><strong>Functions for making a variable symbolic</strong></h2>
<p><code class="highlighter-rouge"><b><font color="#0000FF" size="4">makeConcolicInteger("sym_m", "a")</font></b></code><font size="4">:
This function will make an integer variable symbolic (denoted as <i>sym_m</i>), and initialize it to the concrete integer value <i>a</i>. </font></p>
<p><code class="highlighter-rouge"><b><font color="#0000FF" size="4">makeConcolicChar("sym_c", "c")</font></b></code><font size="4">:
This function will make a char variable symbolic (denoted as <i>sym_c</i>), and initialize it to the concrete char <i>c</i>. </font></p>
<hr />
<h2 id="Specification"><strong>Function for building the FSA</strong></h2>
<p><code class="highlighter-rouge"><b><font color="#0000FF">FiniteStateAutomaton getForwardFSA()</font></b></code>
<font size="4">: This function is used to specify the regular property as a deterministic finite state automaton (FSA). </font></p>
<hr />
<h2 id="FSA"><strong> Functions in class <i>FiniteStateAutomaton</i></strong></h2>
<p><code class="highlighter-rouge"><b><font color="#0000FF">(1). FiniteStateAutomaton()</font></b></code>
<font size="4">: The construction function of the class <b><i>FiniteStateAutomaton</i></b>, and it will return an empty finite state automaton.</font></p>
<p><code class="highlighter-rouge"><b><font color="#0000FF">(2). createState(Point p)</font></b></code>
<font size="4">: Create a state in FSA. The parameter <i>p</i> is a point that specifies a location in the coordinate space. </font></p>
<p><code class="highlighter-rouge"><b><font color="#0000FF">(3). addTransition(Transition t)</font></b></code>
<font size="4">: Add a transition to the FSA, and parameter <i>t</i> is the transition to be added. Specifically, a transition
can be constructed by invoking function <b><i>"new FSATransition(s0, s1, "I")"</i></b>, which means executing event
<i>I</i> can drive state <i>s0</i> to state <i>s1</i>.</font></p>
<hr />
<h2 id="monitor"><strong> Functions in class <i>MonitorWithDFA</i></strong></h2>
<p>The functions in class <i>MonitorWithDFA</i> are used to build a Java monitor.</p>
<p><code class="highlighter-rouge"><b><font color="#0000FF">(1). MonitorWithDFA(FiniteStateAutomaton fsa)</font></b></code>
<font size="4">: Construct a monitor according to the given FiniteStateAutomaton <i>fsa</i>.</font></p>
<p><code class="highlighter-rouge"><b><font color="#0000FF">(2). addSensitiveEvent(String typeName, String methodName)</font></b></code>
<font size="4">: Suppose the monitor is constructed by an FSA <i>fsa</i>, then this function
is used to describe the transition events in <i>fsa</i>. For example, suppose instruction <i>instr</i> is a method call instruction,
if the class name of the invoked method equals parameter <i>typeName</i> and the method name equals parameter <i>methodName</i>,
then <i>instr</i> is a sensitive event of the regular property.</font></p>
<p><code class="highlighter-rouge"><b><font color="#0000FF">(3). addMethodNameChar(String methodName, Char ch)</font></b></code>
<font size="4">: This function associates a sensitive method named <i>methodName</i> with the transition
label <i>ch</i> in the FiniteStateAutomaton <i>fsa</i>. For example, suppose the FiniteStateAutomaton <i>fsa</i> has a transition <i>(s0, s1, "I")</i>,
if we invoked <i>addMethodNameChar("init", "I")</i>, then when we encouter a instruction that invoked a method named <i>init</i>,
state <i>s0</i> will be updated to state <i>s1</i>.</font></p>
<hr />
<h2 id="arguments"><strong>Function for initializing arguments.</strong></h2>
<p><code class="highlighter-rouge"><b><font color="#0000FF">initArgs(String[] args)</font></b></code>
<font size="4">: This function sets the running configuration. The parameter args is an array with seven string elements, and they
represent <b><i>call string bound</i></b>, <b><i>property guided</i></b>, <b><i>refinement flag</i></b>, <b><i>iteration number</i></b>,
<b><i>iteration period</i></b>, <b><i>result file name</i></b>, and <b><i>slicing flag</i></b>,
respectively. For example, suppose the args equals {"1", "1", "0", "-1", "0,0,100,0","","0"}, then the call string bound is 1, and <b>RGSE</b> will run
in the guiding mode with no refinement, no iteration threshold, 100 seconds time threshold
(the types of the four elements are hour, minute, second, millisecond, respectively), empty result file, and no slicing.</font></p>
<hr />
</body>
</html>