32leaves.net

Word generation using an n-dimensional discrete hypercube

This algorithm is something a friend of mine and I have developed quite some time ago (probably a year or so). It might also be already known under some name and I’m not aware of it. None the less it’s an interesting solution to a quite interesting problem.
Suppose that you wanted to generate the words w \in \Sigma^n of the alphabet \Sigma = \{\alpha_0, \alpha_1, \dots, \alpha_m\}. And that you wanted to do that in a parallel manner, such that you had a set of threads where each thread has a unique number out of 0\dots \vert\Sigma\vert^n assigned.
In that case it would be favorable to have a mapping in the form \underbrace{\{k: 0 \leq k < \vert\Sigma\vert^n\}}_S\to\Sigma^n, so that each thread could easily (reading with less computational effort) generate the word it’s supposed to work on. Notice that implicit definition of S:=\{k: 0 \leq k < \vert\Sigma\vert^n\}.
To solve the problem described previously, we start with a function that maps elements of S to points in an n-dimensional discrete hypercube. That mapping V: S\to\{ k: 0\leq k < \vert\Sigma\vert \}^n is defined as follows: V(s) = \begin{bmatrix} \left\lfloor\frac{s}{l^0}\right\rfloor \mod l \\ \left\lfloor\frac{s}{l^1}\right\rfloor \mod l \\ \vdots \\ \left\lfloor\frac{s}{l^{n-1}}\right\rfloor \mod l \end{bmatrix} where l:=\vert\Sigma\vert. This mapping obviously maps a natural number s < \vert\Sigma\vert^n to a point in a discrete n-dimensional hypercube with an edge length of \vert\Sigma\vert. Example: Consider \vert\Sigma\vert = 3 and n = 3. Then we can visualize V as follows:
Now that we have a mapping from a natural number to a point in the hypercube, we need a mapping from a point in the hypercube to the word itself. Such a mapping W: \{ k: 0\leq k < \vert\Sigma\vert \}^n \to \Sigma^n is easy to find. Consider W(p) := \alpha_{p_0}\alpha_{p_1}\dots\alpha_{p_n} where the p_i are the components of the vector p and \alpha_i \in \Sigma.
So our final mapping F: S\to\Sigma^n is F:=W\circ V and exactly what we desired. One might notice that F must be surjective so that each word is computed if there are just enough threads. To prove that, we’ll prove that V as well as W is surjective (since the functional composition of two surjective functions is surjective as well).
Theorem: V is surjective, so that \forall v \in \{ k: 0\leq k < \vert\Sigma\vert \}^n : \exists x \in S : V(x) = v.
Proof: Let l:=\vert\Sigma\vert, u_i\in\mathbb{N}, y\in S and v:=\begin{bmatrix} v_1 & \dots & v_n\end{bmatrix}^T. Assume that y = v_1\cdot l^0 + \dots + v_n\cdot l^{n-1}, then

V(y) = 	\begin{bmatrix}  		v_1+\underbrace{\dots+v_{n}\cdot l^{n-1}}_{u_1\cdot l} \mod l \\ 		\vdots \\ 		\underbrace{\left\lfloor\frac{v_1\cdot l^0 + \dots}{l^{n-1}}\right\rfloor}_{u_n\cdot l} + v_n \mod l 	\end{bmatrix} (1)
= \begin{bmatrix}  		v_1 \mod l & \dots & v_n \mod l 	\end{bmatrix}^T (2)
= \begin{bmatrix} v_1 & \dots & v_n\end{bmatrix}^T = v (3)

The transition from (1) to (2) is allowed as u_i\cdot l\mod l = 0. Similar goes for the equivalence of (2) and (3): v_i \mod l = v_i as v_i \leq l.

Theorem: W is surjective, so that \forall w \in \Sigma^n : \exists v \in \{ k: 0\leq k < \vert\Sigma\vert \}^n : W(v) = w.
Proof: Let w:=\alpha_{v_1}\dots\alpha_{v_n} then the vector v=\begin{bmatrix}v_1 & \dots & v_n\end{bmatrix} (which obviously fullfils W(v)=w) must exist, since v_i < \vert\Sigma\vert and v\in \{ k: 0\leq k < \vert\Sigma\vert \}^n.
So the mapping F is surjective and does exactly what we want. I consider that solution to be a particular elegant one and wanted of post it for about a year now. Finally I found some spare time to do so. If you use that solution, find a mistake or find it somewhere else (maybe even previously described) please drop a comment.

Soap Bubble Bot

During my studies at the HFU, I have to participate in at least two semester projects. This time we built a new USB interface for some pretty old hardware. That old hardware is a robot arm built in 80′s (there is “Made in West Germany” written on it). I’ve blogged about it before.
Today we got to present our work. But how do you show something as abstract as interface hardware/software? So we came up with that demo which we consider pretty neat: we taught the robot arm to make soap bubbles. Well, we used a bunch of ruby scripts to grad the events generated by a gamepad (HID device) and interpreted them, so that one can control the arm. We also taped something (I’d call a soap bubble device) at the front of robot. Add some of the soap fluid and we could’ve made soap bubbles manually. But that’s too easy. So we added a sequence of positions (one of the firmware’s features) and used that to do the work. Video’s after the break.

LogicAnalyzer – extensible logic debugging

In the past few months it has become quite on this blog. That’s not because I wasn’t involved in any activity, but rather because I was too involved in one (building a quadrocopter). During that particular activity we started using a logic analyzer. There is a great open source project building such a device (originally here). Unfortunately for quite some time it was out of stock. So we set on to build one ourselves. In that process I started writing some client software for it, since there was a lack of extensible, open source, logic analyzer client software. In the meantime, the Open Workbench Logic Sniffer was in stock again. So we ordered two of them. At the time they arrived, the LogicAnalyzer was pretty much usable.
While designing the LogicAnalyzer, I had three major goals in mind:

  1. Extensibility: integrating new devices should be as easy as possible. Generally speaking, integrating any kind of data source should be easy.
  2. Clean UI: some logic analyzer client software that is around has a pretty cluttered UI. The LogicAnalyzer UI should be clean and intuitive.
  3. Architecture: in order to achieve the required extensibility and to enhance maintainability, a good and clean architecture is required.

All goals have been met (although one might discuss how well goal three has been reached – that’s in the eye of the beholder).

LogicAnalyzer is built using the Eclipse Rich Client Platform. This powerful platform provides mechanisms to extend applications built using it. So we’re using the extension point mechanism of Eclipse to provide the required extensibility. Special focus has been put on a clean API and unobtrusive interfaces. By using Eclipse RCP, we also gain multi-platform support. LA runs on Mac OSX, Linux and Windows.

The clean UI is achieved by only showing what’s currently required. When you open LogicAnalyzer, all you’ll see is the button to get you started. The tools integrated into the program may require a UI, which is only shown when they’re selected. We wanted to maximize the amount of pixels available to show what’s really important: the data we’re visualizing.

An important (but simple) rule during the design phase, has been a clear separation of concerns. Thus we’ve clearly separated UI from business logic. Most components are connected using Eclipse mechanisms (e.g. extension points). A lot has been designed against interfaces (where appropriate). Those measures resulted in a clean structure and good maintainability.
If you want to know more (such as a list of features) or want to give it a try, I recommend that you have a look at LogicAnalyzers homepage. Some numbers for those interested: the initial commit was roughly 10k lines of code written in two weeks. Still, so far we’ve experienced only few (known but unfixed) bugs.

Making the world a safer place: self-verifying SMC

We all use code-generators, no matter if we love or hate them (or do both). But for most compilers you simply have to trust that they work correctly and do what they’re supposed to do. They typically do not provide any sort of proof for their correctness. Well, the SMC is different in that regard. It can generate verification code for its C backend.
The idea of self-verifying compilers it not completely new. Several methods have been proposed for this task, proof-carying code and credible compiler to name a few. What I’m doing here is some mixture of both (with a bit more of the credible compiler – altough the SMC is no optimizing compiler, so there is only a single transformation involved). Basically once we generated C code out of the FSM description, we have two (possibly different) FSMs. The one we described and the one SMC generated. The intuitive perception of those two FSMs being equal, is that their languages (dented by \mathcal{L}(F)) are equal. But how do we show that?
For our purpose it’s enough to show that the two transition functions are equal, as we only care about the generated FSM behaving exactly as the described one does. That still leaves us with the problem that we have to unobtrusively check the generated FSM.
Let us define p=(t_1, \dots, t_n), t_i = ((s, \sigma), (s', A_{in}, A_{out}))\in\delta to be a sequence of transitions (called path or trace). We’ll call a path loop free if \forall t: \neg\exists t': t = t' \vee s_t \neq s_{t'} holds – meaning that there are no two transitions within a path having the same start state.
Finally we accept the two FSMs to be equal iff for all loop-free paths in the original FSM, there exists an equivalent path in the generated machine. Following we accept the SMC to work correctly if the two FSMs (orignal one and generated one) are equal.
Generating the traces of the original FSM is a rather trivial task. We already have a good structure to work on (the SMC AST). That’s not the case with the generated FSM. First of all generating the trace must be unobtrusive. We must be sure that our instrumentation does alter the behavior of the FSM. We can accept that a statement of the form

1
printf("12345678");

generally does not alter the behavior, if placed appropriate. So we simply place print statements (with a unique ID) at each transition and action. Then we generate code that causes the FSM to transit along the previously determined paths.
If everything goes right, executing that code should cause a sequence of IDs to be printed. In case the SMC works correctly that sequence should be identical to those produced by traces of the original FSM.

To use this verification mechanism, run the SMC with the cverify backend and execute the generated _checker.sh script. That script either ends with “NO ERRORS FOUND” (which should always be the case), with a list of traces which the generated FSM did not perform. Additionally a checker.log file is generated which contains entries like this:

1
2
3
[ ] AST_Transition(_INIT,RT,List(AST_ConstEqCondition(CMD__MODE__RT)),AST_Actions(Some(List(clr)),None)) AST_Transition(RT,_ERR,List(AST_NegatedCondition(AST_PredicateCondition(command))),AST_Actions(None,None))
[!] A98601 T-93118478 T-1152986909 ;
[?] A98601 T-93118478 T-1152986909 ;

where the line marked by the exclamation mark denote the trace of the original FSM, as opposed to question mark which marks trace of the generated FSM.

Ahh, and there is yet another new feature, the SMC can now generate a NuSMV model. Of course that’s all in the repository.

State machine compiler

As mentioned in one my previous posts, next semester I’m going to participate in a project where we’re supposed to build a new interface to existing roboting hardware. To describe the protocol that is spoken between the computer and that hardware interface, I wanted to use some sort of DFA. I also wanted avoid having to implement that DFA in the different programming languages involved in the project. Especially since such implementations tend to diverge over time.
So I sat down and wrote something I call the state machine compiler. It allows the specification of a so called predicate deterministic finite automaton. Such a PDFA can be compiled to C or Java code – or to whichever language one writes a backend for. I won’t go into detail here, as I’ve written a manual which explains everything in detail.
You can grab the source code from subversion (username: guest, password: guest). As usual it’s published under CC-BY-SA. Be aware that this is considered work in progress, so the generated code may still be far from being optimal.

Generating syntax diagrams from Scala parser combinators

Scala parser combinators are a powerful concept which allow you to write parsers with the standard Scala distribution. They’re implemented as an internal DSL which makes them feel naturally in the language. As mentioned before I’m currently writing some sort of a state machine compiler. As I plan to write some documentation for that software (which actually is kind of rare :-P) I need some way to describe the syntax. Besides EBNF, syntax diagrams are a neat way to do that. The external DSL which is used to describe the state machines is directly written using the parser combinator, so I had figure out a way to generate syntax diagrams as well as EBNF out of them.
My first approach was to pattern match the resulting Parser structure. But unfortunately the combinators themselves are mostly modeled as a function, thus do not appear in the resulting object graph. So I decided to write a Scala compiler plugin and run thru the AST. Basically all this software does is to transform trees from the AST to some intermediate expression structure to a graphing tree one. This approach suffers some limitations and I made some assumptions as well:

  • The name of the class which contains the production rules must equal the filename without “.scala”
  • Production rules must not be named: “stringWrapper”, “literal”, “regex”, “Predef”, “r” or “accept”
  • def production rules must not have parameters, otherwise they’re not considered to be production rules
  • production rules defined via val will appear twice (this is most likely a bug)

All in all this implementation works in my case, but might not work for others. This more of a quick hack than carefully engineered software, but it proofs the concept and gets the job done.

With the ability to draw syntax diagrams and having the expression tree structure at hand (which can be seen as an AST for EBNF) writing an EBNF parser (which is semi ISO/IEC 14977 : 1996(E) compatible) and feeding the diagram generator with the result was a snap.
So let’s consider the following example (which actually is the EBNF parser I wrote):

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
def start: Parser[List[ProductionRule]] = syntax_rule*
def syntax_rule = meta_identifier ~ '=' ~ definitions_list ~ ';' ^^ {
  case name ~ _ ~ expr ~ _ => ProductionRule(name, expr)
}
def meta_identifier = """[a-zA-Z0-9]+"""r
def definitions_list:Parser[Expression] = (single_definition ~ (('|' ~ single_definition)*)) ^^ {
  case t ~ o => OrExpression(t :: o.map(_ match { case _ ~ x => x }))
}
def single_definition = (primary ~ (((","?) ~ primary)*)) ^^ {
  case t ~ o => SeqExpression(t :: o.map(_ match { case _ ~ x => x }))
}
def primary: Parser[Expression] = optional_sequence | repeated_sequence | grouped_sequence | terminal_string | meta_identifier ^^ {
  case s => RuleRefExpression(s)
}
def optional_sequence = "[" ~ definitions_list ~ "]" ^^ {
  case _ ~ os ~ _ => OptionExpression(os)
}
def repeated_sequence = "{" ~ definitions_list ~ "}" ^^ {
  case _ ~ rs ~ _ => ZeroToManyExpression(rs)
}
def grouped_sequence = "(" ~ definitions_list ~ ")" ^^ {
  case _ ~ gs ~ _ => gs
}
def terminal_string = (""""[^"\\\r\n]*(?:\\.[^"\\\r\n]*)*" """r) ^^ {
  case s => LiteralExpression(s)
}

The corresponding EBNF expression generated by this software is:

1
2
3
4
5
6
7
8
9
10
start = { syntax_rule };
syntax_rule = ( '[a-zA-Z0-9]+' '=' ( single_definition { ( '|' single_definition ) } ) ';' );
meta_identifier = '[a-zA-Z0-9]+';
definitions_list = ( ( primary { ( [ ',' ] primary ) } ) { ( '|' single_definition ) } );
single_definition = ( ( optional_sequence | repeated_sequence | grouped_sequence | terminal_string | meta_identifier ) { ( [ ',' ] primary ) } );
primary = ( ( '[' definitions_list ']' ) | ( '{' definitions_list '}' ) | ( '(' definitions_list ')' ) | '"[^"\\\r\n]*(?:\\.[^"\\\r\n]*)*" ' | '[a-zA-Z0-9]+' );
optional_sequence = ( '[' ( single_definition { ( '|' single_definition ) } ) ']' );
repeated_sequence = ( '{' ( single_definition { ( '|' single_definition ) } ) '}' );
grouped_sequence = ( '(' ( single_definition { ( '|' single_definition ) } ) ')' );
terminal_string = '"[^"\\\r\n]*(?:\\.[^"\\\r\n]*)*" ';

And of course the syntax diagrams we wanted:

So far the syntax diagram generator understands two options:

  • -P:virtual:rule01,...,ruleN: declares rule01,…,ruleN to be virtual rules which causes them to be resolved wherever they’re referenced. Be aware that recursive virtual rules are only resolved to one level
  • -P:depth:N: resolve rule references until a depth of N (recursive rules are only resolved for one level)
If you’re interested in the code you can grab it from this SVN repository (username: guest, password: guest). You’ll need Scala as well as Batik to run it.
Creative Commons License
SyntaxDiagramGenerator is licensed under a Creative Commons Attribution-Share Alike 3.0 Unported License

Visualizing Sorting Algorithms – my shot

These days I have to write some sort of reference card for basic sorting algorithms. Of course I wanted some sort of visualization of those algorithms on that card. The coolest sorting algorithm visualization I’ve seen so far has been created by Aldo Cortesi. He used Cairo to draw his stuff (according to his post learning Cairo was the whole point of this excercise).
Personally I still found those diagrams pretty hard to read if you really wanted to follow the algorithm. And of course I wanted to do something with Cairo, too. So I decided to rewrite the whole thing in C. My version shows distinct sections for each loop iteration (as most of those algorithms can be followed by thinking in that iterative loop way). In the diagrams below each number denotes the loop nesting level while B stands for being and E for end.
The source can be downloaded here and is under CC-BY-SA.

Controlling a robot arm using an ez430 Chronos

A few days ago the ez430 Chronos I ordered from Farnell was delivered. This particular piece of hardware is an evaluation platform for the MSP430 (or the MSP430 as a CC430F6137 SoC to be more precise) which comes as a sports watch. It’s got some pretty neat features such as a temperature sensor, accelerometers on all three axis (which is why I’m using it here) and an RF transceiver built in. The first thing I did to it was to enable the watch to display the current time binary encoded.
After getting this to work (which was not that hard at all) I moved on to trying to get some data using the RF link. In the ez430 Chronos Wiki someone posted a Python program which polls the RF hub for accelerometer data. Having a Mac and not wanting to spend hours on getting pyserial to work, I wrote my own version in Ruby.

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
require 'rubygems'

# on my machine a simple require does not work for this library
Kernel.require 'serialport'


SERIAL = SerialPort.new ARGV[0], 115200
SERIAL.read_timeout = 1000
def serial(data); data.each {|c| SERIAL.putc(c) }; SERIAL.flush end

# start access point
serial([0xFF, 0x07, 0x03])

while(true)
  # request the data
  serial([0xFF, 0x08, 0x07, 0x00, 0x00, 0x00, 0x00])

  accel = SERIAL.read(7)
  unless accel.nil?
    accel = accel.scan(/./).map {|c| c[0] }

    if accel[3] == 1
      puts accel[4..6].join(" ")
      STDOUT.flush
    end
  end
end

SERIAL.close

That’s pretty nice, but I wanted some real time graphs of the data, so a half an hour later I got a short Processing sketch running which does exactly that.

Next semester I’ll participate in a project in which we’ll built a new hardware interface to some pretty old robot arm hardware (it states “Made in West Germany”, that’s quite some time ago). In order to do that we need some sort of protocol to communicate with the new hardware interface. In preparation for that project I wrote a simulator for the robot (actually that’s supposed to be a part of the project, but I simply couldn’t resist) which uses an early draft of that particular protocol. Just to have that mentioned, the protocol itself is described as a state machine in a DSL which can be compiled to virtually any programming language. I’ll probably write a post about that nice piece of Scala code at some later time.
So with a working robot arm simulator, a watch which has accelerometers built in and is capable of wireless communication what else could I’ve done than to combine those two. That said I got to work and enhanced the script above to communicate with the simulator. About an hour later I got the first movements controlled by the accelerometer data of the watch. You might have seen the video already, if not go and watch it :-)
Update: We had some spare time to spent and did some really basic proof of concept with the real hardware. Here we go:

Readonly hardware IRC client

Right after we got the network running on my board (see my previous post) I got the board of the talented hacker mentioned before and started to hack a small read-only IRC client for it (after having a look at RFC1459 and RFC2812. About an hour later I was able to connect to a server, join a channel and listen for messages which are displayed on the OLED display. Unfortunately the display is broken on that particular board. But none the less, there is a lot of cool stuff ahead.
Again we have some screenshots:

Getting the network of my LM3S6965 board to work

I’ve had this board for about a 1.5 years. All that time I was disliked the fact that the ethernet was not working. No matter what I tried, what example I flashed nothing helped. Today I learned why: the hardware’s simply broken.
That’s no guess too far away, but being a software guy that’s just an unreachable world to me.
Thankfully that’s not the case for a friend of mine. He’s a talented hacker (from today on I know how talented :P) and he got this fixed. All the time I was like: “hey, if that’s so easy someone else would have done it already instead of buying that super-expensive Pulse Jack Ethernet Transformer hardware”. None the less he pushed forward and got it to work. As usually pictures say more than a thousand words, so here we go:
« Previous PageNext Page »
Fork me on GitHub