Skip to content

Commit a8db48c

Browse files
robby-phdrobby-phd
committed
Refactored ParseTree and PredictiveTable, and added DFA, NFA, and NGrammar (N=normalized).
1 parent deedb30 commit a8db48c

File tree

8 files changed

+1057
-60
lines changed

8 files changed

+1057
-60
lines changed

‎library/shared/src/main/scala/org/sireum/automaton/Dfa.scala‎

Lines changed: 169 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,169 @@
1+
// #Sireum
2+
/*
3+
Copyright (c) 2017-2026,Robby, Kansas State University
4+
All rights reserved.
5+
6+
Redistribution and use in source and binary forms, with or without
7+
modification, are permitted provided that the following conditions are met:
8+
9+
1. Redistributions of source code must retain the above copyright notice, this
10+
list of conditions and the following disclaimer.
11+
2. Redistributions in binary form must reproduce the above copyright notice,
12+
this list of conditions and the following disclaimer in the documentation
13+
and/or other materials provided with the distribution.
14+
15+
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
16+
ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
17+
WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
18+
DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR
19+
ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
20+
(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
21+
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
22+
ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
23+
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
24+
SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
25+
*/
26+
27+
package org.sireum.automaton
28+
29+
import org.sireum._
30+
import org.sireum.U32._
31+
32+
@datatype class Dfa[E](val initial: Z, val accepting: HashSSet[Z], val g: Graph[Z, E]) {
33+
34+
/** Minimizes this DFA using partition refinement.
35+
*
36+
* Iteratively splits groups of states whose outgoing transitions
37+
* disagree on which group the target belongs to, until stable.
38+
*
39+
* @param sortEdge comparison function for sorting edge signatures;
40+
* given two `(label, targetGroup)` pairs, returns
41+
* `T` if the first should come before the second
42+
*/
43+
def minimize(sortEdge: ((E, Z), (E, Z)) => B @pure): Dfa[E] = {
44+
val states = g.nodesInverse
45+
if (states.size <= 1) {
46+
return this
47+
}
48+
var partition = ISZ[ISZ[Z]]()
49+
var acceptGroup = ISZ[Z]()
50+
var nonAcceptGroup = ISZ[Z]()
51+
for (s <- states) {
52+
if (accepting.contains(s)) {
53+
acceptGroup = acceptGroup :+ s
54+
} else {
55+
nonAcceptGroup = nonAcceptGroup :+ s
56+
}
57+
}
58+
if (nonAcceptGroup.nonEmpty) {
59+
partition = partition :+ nonAcceptGroup
60+
}
61+
if (acceptGroup.nonEmpty) {
62+
partition = partition :+ acceptGroup
63+
}
64+
var changed: B = T
65+
while (changed) {
66+
changed = F
67+
var stateToGroup = HashSMap.empty[Z, Z]
68+
var gi: Z = 0
69+
while (gi < partition.size) {
70+
for (s <- partition(gi)) {
71+
stateToGroup = stateToGroup + s ~> gi
72+
}
73+
gi = gi + 1
74+
}
75+
var newPartition = ISZ[ISZ[Z]]()
76+
for (group <- partition) {
77+
if (group.size <= 1) {
78+
newPartition = newPartition :+ group
79+
} else {
80+
var sigMap = HashSMap.empty[ISZ[(E, Z)], ISZ[Z]]
81+
for (s <- group) {
82+
var sig = ISZ[(E, Z)]()
83+
for (edge <- g.outgoing(s)) {
84+
val de = edge.asInstanceOf[Graph.Edge.Data[Z, E]]
85+
sig = sig :+ (de.data, stateToGroup.get(de.dest).get)
86+
}
87+
sig = ops.ISZOps(sig).sortWith(sortEdge)
88+
sigMap.get(sig) match {
89+
case Some(ss) => sigMap = sigMap + sig ~> (ss :+ s)
90+
case _ => sigMap = sigMap + sig ~> ISZ(s)
91+
}
92+
}
93+
for (subGroup <- sigMap.values) {
94+
newPartition = newPartition :+ subGroup
95+
}
96+
if (sigMap.size > 1) {
97+
changed = T
98+
}
99+
}
100+
}
101+
partition = newPartition
102+
}
103+
var stateToGroup = HashSMap.empty[Z, Z]
104+
var gi: Z = 0
105+
while (gi < partition.size) {
106+
for (s <- partition(gi)) {
107+
stateToGroup = stateToGroup + s ~> gi
108+
}
109+
gi = gi + 1
110+
}
111+
val initialGroupIdx = stateToGroup.get(initial).get
112+
if (initialGroupIdx != z"0") {
113+
var reordered = ISZ[ISZ[Z]]()
114+
reordered = reordered :+ partition(initialGroupIdx)
115+
var ri: Z = 0
116+
while (ri < partition.size) {
117+
if (ri != initialGroupIdx) {
118+
reordered = reordered :+ partition(ri)
119+
}
120+
ri = ri + 1
121+
}
122+
partition = reordered
123+
stateToGroup = HashSMap.empty[Z, Z]
124+
gi = 0
125+
while (gi < partition.size) {
126+
for (s <- partition(gi)) {
127+
stateToGroup = stateToGroup + s ~> gi
128+
}
129+
gi = gi + 1
130+
}
131+
}
132+
var newAccepting = HashSSet.empty[Z]
133+
var ai: Z = 0
134+
while (ai < partition.size) {
135+
if (accepting.contains(partition(ai)(0))) {
136+
newAccepting = newAccepting + ai
137+
}
138+
ai = ai + 1
139+
}
140+
var newG = Graph.empty[Z, E]
141+
var ni: Z = 0
142+
while (ni < partition.size) {
143+
newG = newG * ni
144+
ni = ni + 1
145+
}
146+
var ei: Z = 0
147+
while (ei < partition.size) {
148+
val rep = partition(ei)(0)
149+
for (edge <- g.outgoing(rep)) {
150+
val de = edge.asInstanceOf[Graph.Edge.Data[Z, E]]
151+
val targetGroup = stateToGroup.get(de.dest).get
152+
newG = newG.addDataEdge(de.data, ei, targetGroup)
153+
}
154+
ei = ei + 1
155+
}
156+
return Dfa(initial = z"0", accepting = newAccepting, g = newG)
157+
}
158+
159+
}
160+
161+
object Dfa {
162+
val maxChar: C = conversions.U32.toC(u32"0x0010FFFF")
163+
164+
@pure def isReject(edge: Graph.Edge[Z, (C, C)]): B = {
165+
val e = edge.asInstanceOf[Graph.Edge.Data[Z, (C, C)]]
166+
return e.source == e.dest && e.data._1 == '\u0000' && e.data._2 == maxChar
167+
}
168+
169+
}

‎library/shared/src/main/scala/org/sireum/automaton/Nfa.scala‎

Lines changed: 153 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,153 @@
1+
// #Sireum
2+
/*
3+
Copyright (c) 2017-2026,Robby, Kansas State University
4+
All rights reserved.
5+
6+
Redistribution and use in source and binary forms, with or without
7+
modification, are permitted provided that the following conditions are met:
8+
9+
1. Redistributions of source code must retain the above copyright notice, this
10+
list of conditions and the following disclaimer.
11+
2. Redistributions in binary form must reproduce the above copyright notice,
12+
this list of conditions and the following disclaimer in the documentation
13+
and/or other materials provided with the distribution.
14+
15+
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
16+
ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
17+
WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
18+
DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR
19+
ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
20+
(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
21+
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
22+
ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
23+
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
24+
SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
25+
*/
26+
27+
package org.sireum.automaton
28+
29+
import org.sireum._
30+
31+
/** NFA fragment used in Thompson's construction.
32+
*
33+
* Uses `Graph[Z, Option[E]]` where `None` labels represent
34+
* epsilon transitions and `Some(e)` labels represent
35+
* data-carrying transitions.
36+
*/
37+
@datatype class Nfa[E](
38+
val initial: Z,
39+
val accept: Z,
40+
val g: Graph[Z, Option[E]],
41+
val nextState: Z
42+
) {
43+
44+
/** Converts this NFA to a DFA via the subset construction algorithm.
45+
*
46+
* @param splitTransitions abstracts label-specific interval splitting;
47+
* given collected `(label, targetState)` pairs,
48+
* returns `(label, targetStates)` groups
49+
*/
50+
def toDfa(splitTransitions: ISZ[(E, Z)] => ISZ[(E, ISZ[Z])]): Dfa[E] = {
51+
val startStates = Nfa.epsilonClosure(ISZ(initial), g)
52+
var stateMap = HashSMap.empty[ISZ[Z], Z]
53+
stateMap = stateMap + startStates ~> z"0"
54+
var worklist = ISZ(startStates)
55+
var dfaNextState: Z = 1
56+
var accepting = HashSSet.empty[Z]
57+
var edges = ISZ[(E, Z, Z)]()
58+
if (ops.ISZOps(startStates).contains(accept)) {
59+
accepting = accepting + z"0"
60+
}
61+
while (worklist.nonEmpty) {
62+
val current = worklist(0)
63+
worklist = ops.ISZOps(worklist).tail
64+
val currentDfa = stateMap.get(current).get
65+
var transitions = ISZ[(E, Z)]()
66+
for (s <- current) {
67+
for (edge <- g.outgoing(s)) {
68+
val de = edge.asInstanceOf[Graph.Edge.Data[Z, Option[E]]]
69+
de.data match {
70+
case Some(label) =>
71+
transitions = transitions :+ (label, de.dest)
72+
case _ =>
73+
}
74+
}
75+
}
76+
val intervals = splitTransitions(transitions)
77+
for (interval <- intervals) {
78+
val targetClosure = Nfa.epsilonClosure(interval._2, g)
79+
if (targetClosure.nonEmpty) {
80+
var targetDfa: Z = -1
81+
stateMap.get(targetClosure) match {
82+
case Some(n) =>
83+
targetDfa = n
84+
case _ =>
85+
targetDfa = dfaNextState
86+
dfaNextState = dfaNextState + 1
87+
stateMap = stateMap + targetClosure ~> targetDfa
88+
worklist = worklist :+ targetClosure
89+
if (ops.ISZOps(targetClosure).contains(accept)) {
90+
accepting = accepting + targetDfa
91+
}
92+
}
93+
edges = edges :+ (interval._1, currentDfa, targetDfa)
94+
}
95+
}
96+
}
97+
var dfaG = Graph.empty[Z, E]
98+
var ni: Z = 0
99+
while (ni < dfaNextState) {
100+
dfaG = dfaG * ni
101+
ni = ni + 1
102+
}
103+
for (edge <- edges) {
104+
dfaG = dfaG.addDataEdge(edge._1, edge._2, edge._3)
105+
}
106+
return Dfa(initial = z"0", accepting = accepting, g = dfaG)
107+
}
108+
109+
}
110+
111+
object Nfa {
112+
113+
/** Merges all nodes and edges from `b` into `a`. */
114+
def mergeGraphs[E](a: Graph[Z, E], b: Graph[Z, E]): Graph[Z, E] = {
115+
var g = a
116+
for (node <- b.nodesInverse) {
117+
g = g * node
118+
}
119+
for (edge <- b.allEdges) {
120+
g = g.addEdge(edge)
121+
}
122+
return g
123+
}
124+
125+
/** Concatenates two NFA fragments via an epsilon transition. */
126+
def concat[E](a: Nfa[E], b: Nfa[E]): Nfa[E] = {
127+
var g = mergeGraphs(a.g, b.g)
128+
g = g.addDataEdge(None[E](), a.accept, b.initial)
129+
return Nfa(initial = a.initial, accept = b.accept, g = g, nextState = b.nextState)
130+
}
131+
132+
/** Computes the epsilon-closure of a set of NFA states. */
133+
def epsilonClosure[E](states: ISZ[Z], g: Graph[Z, Option[E]]): ISZ[Z] = {
134+
var result = HashSSet.empty[Z]
135+
for (s <- states) {
136+
result = result + s
137+
}
138+
var worklist = states
139+
while (worklist.nonEmpty) {
140+
val s = worklist(0)
141+
worklist = ops.ISZOps(worklist).tail
142+
for (edge <- g.outgoing(s)) {
143+
val de = edge.asInstanceOf[Graph.Edge.Data[Z, Option[E]]]
144+
if (de.data.isEmpty && !result.contains(de.dest)) {
145+
result = result + de.dest
146+
worklist = worklist :+ de.dest
147+
}
148+
}
149+
}
150+
return ops.ISZOps(result.elements).sortWith((a, b) => a < b)
151+
}
152+
153+
}

0 commit comments

Comments
 (0)