« April 2005 | Main | June 2005 »

May 27, 2005

[Paper reviews] Interesting TOSE paper to read

[Software Assurance by Bounded Exhaustive Testing] Looks alot like some idaes we've been kicking around and may have some insights we can build on.

Posted by jones at 09:33 AM | Comments (0)

May 26, 2005

[Misc.] Visiting Sacramento CA with 2-year-old twins

We recently visited Sacramento, CA with our 2-year-old twins. We stayed at Oxford Suites in Roseville which has these suites with a pocket door that can seperate the big-person sleeping area from the little person sleeping area. Even better, the big person sleeping area was adjacent to the door. We saw lots of people with children < 5 years old. Our room was either fairly soundproof (meaning the neighbors didn't hear us either) or our neighbors were very quiet.

We visited Fairytale Town for most of a morning. It was ideal. Lots of slides and things for a 2-year-old to play on. Maybe even better than Disney(land|world).

We drove up to Nevada City (one of the places I served on my LDS mission, so it was nice to be there again) and further north on Highay 49. Just before the Yuba river fork crossing, there is a wheelchair accesible trail that goes for a mile or two in each direcation. And, as we all know, that means the trail is perfect for other uses such as strollers. The walk through the woods would have been ideal--it even had a set of stairs off to the side for the twins to "play" on--except for the mosquitos. So if you make the drive, take mosquito repellant. I think going down to Coloma and visiting the gold discovery site might have been better.

We also visited the Oakland LDS temple for a wedding (which is why we were in Sacramento in the first place). It was pretty rough keeping the twins out of the sun and avoiding sunburn. There was a nice (and sunny) garden, plaque and statue conveying the idea of Jesus Christ with the children. It was touching with the twins. Not optimal for an all-day wedding type visit, but would be worth a drive to see it and appreciate the little ones if one were visiting San Fransisco anyway.

Posted by jones at 07:27 PM | Comments (0)

[Misc.] Zinc, model checking, google and me

[Google Search: zinc model checker ] Earlier today, I was searching for a reference topological sorting in a tool called "zinc" which I think is a model checker. You can imagine my surprise when a google for "zinc model checker" brought up my fair blog as link number 5. My entries on a zinc nasal membrene delivery patent and model checking were both made in February 2004 which puts them on the same web page. Certainly worth a pause in paper revision to make a note of it.

Posted by jones at 03:27 PM | Comments (0)

May 18, 2005

[Tech Support] How to modify bogor

  1. Download the bogor core source file from KSU. Un jar it (jar xf)
  2. Fire up eclipse, wait.
  3. Select file -> import -> existing project into workspace.
  4. Um, pick the bogor core project.
  5. Click (finish | ok | accept | yes)* until done.
  6. On some Macs, you will need to make sure that your JRE System Library is JVM 1.5.


Posted by jones at 03:11 PM | Comments (0)

May 13, 2005

[Tech Support] Running Bogor on Windows, Linux and/or Mac OS X Tiger

A guide to installing Bogor on Windows, Linux and Mac OS X written by Eric Mercer.

He has also got a guide to using the Bogor command line interface and doing linear temporal logic (LTL) model checking in Bogor.

The remainder of this entry is deals with Mac OS X only.

My goal here is to run the latest and greatest Bogor (a model checker written in Java) on my Mac. The first step in this process is to install the latest and greatest Eclipse...

The first step is to get eclipse running on the new Java with GEF support. Note that the eclipse-mac group at Google is really helpful.


  1. Download the J2SE 5.0 release from apple: http://www.apple.com/support/downloads/java2se50release1.html
  2. install it.
  3. Follow the instructions for making J2SE 5.0 the default Java platform
  4. Download Eclipse 3.1M6 for Mac OS X Carbon. Drop the new eclipse folder where ever you'd like.
  5. I added a line to my eclipse/Eclipse.app/Contents/Info.plist file to point Eclipse at my freshly installed Java 1.5 VM, as suggested by Cyrill Rüttimann on the Eclipse-Mac google group:

    <key>Eclipse</key>
    <array>
    <string>-vm</string>
    <string>/System/Library/Frameworks/JavaVM.framework/Versions/1.5.0/Commands/java</string>
    ...

    Except I added the new lines before the rest of the Eclipse options rather than after.
  6. In eclipse, do this "Window --> Preferences --> Java (expand this tree item)--> Compiler. Set "Compiler compliance level", "Generated .class file compatibility", and "Source compatibility" to 5.0." as described in the release notes for bogor
  7. now the new eclipse runs fine on the new java.
  8. Next update your GEF in Eclipse. You can do this clicking: help-> software updates -> Find and install -> check "Search for new features to install" -> Next -> check "eclipse.org update site" -> Finish. Then you wait while the updater searches. Expand the "eclipse.org update site" item. Scroll down and find GEF 3.0.1. Make sure it is selected, and you may unselect the others--your call. Click the appropriate sequence of (next | finish | ok | install | yes)* until it is installed.

The next step is to get Bogor working.


  1. Close eclipse if it is open.
  2. Download the latest bogor binary. I used bogor-bin-20050414.jar.
  3. Move or copy your new bogor-bin-20050414.jar into your eclipse/plugins directory. In your ecplipse/plugins directory, do a jar xf bogor-bin-20050414.jar to extract the files.
  4. Open eclipse and test that bogor works by creating a new simple project.
  5. Open a file with a .bir (or .BIR) extension in your new simple project.
  6. You should see the root beer mug icon with BIR next to the file name.
  7. Download the bir dining philosophers example and paste it into your eclipse editor.
  8. Save the file
  9. Right click in the bir text editor (for those of you Mac users that actually use a one-button mouse, you'll have to use some combination of shift or control or apple or option and a mouse click) and choose "Model check -> default configuration" from the bottom of the resulting menu.
  10. if all went well, you should see a Bogor status window with 14 transitions, 10 states and 5 matched.

The next instruction sequence describes how I obtained the Bogor source and imported it into my Eclipse installation. The point here is to be able to modify Bogor, on a Mac, using Eclipse as the IDE.


  1. Download the bogor source jar's, all five of them.
  2. Put them in a directory which is not contained in your eclipse workspace directory.
  3. In eclipse, do "file -> New -> Project -> Plug-in Development -> Plug-in from existing JAR archives" And click "next".
  4. Choose to "add external..." JARs. Navigate your way to the recently downloaded JAR files.
  5. Add them one by one, or do the same thing using a less tedious method if you know one (which I don't). And click "next"
  6. Fill in some project details and click "next" etc until done.
  7. in the "package explorer" make sure that "JRE System Library" is set to JVM 1.5. This may or may not be your default JVM.


The long-term plan is to get the Bogor sources and integrate it with a bdd package so that one can do symbolic model checking on BIR models. It looks like JavaBDD is going to be the package for me. It has good OS X support (which means it has good Windows and Linux support, of course), supports CUDD and BUDDY and has a pure Java package if that's what you want to do.

Posted by jones at 02:13 PM | Comments (1)

[Research] Tracking Bees with Radar

[Wired News: Decoding Bees' Wild Waggle Dances] I did some work with Jacob Sorber on using honeybee cooperation mechanisms in parallel error detection. This work maybe the next piece in the honeybee puzzle, which is, when a bee leaves the hive, where does it go? Tracking a bee in free flight across the countryside is a surprisingly difficult problem to solve.

Posted by jones at 01:22 PM | Comments (0)

May 12, 2005

[Research] What does P-Complete mean?

[NC-Reducibility and P-Completeness] It seemed odd to me to define P-completeness. But I think I get it now.
The class NC is the class of problems that are solvable "efficiently" by a polynomial number of processors. The more precise definition is on the webpage.

The class P is what you'd think it would be, the class of problems that are solvable in polynomial time (and space) on a deterministic Turing machine. The question here is , are all problems in P in NC? That is, are all problems that can be effiicently solved by a deterministic Turing machine efficiently parallelizable?

The answer to that question is not clear, but, you can take the hardest problems in P and show that if one of them is in NC, then all of P is in NC. That is, if one of these hardest problems is efficiently parallelizable, then everything in P is efficiently parallelizatable.

So you'd expect some kind of reduction for showing that problem is P-complete by reducing a known P-complete problem to it. Its in the linked page.

Posted by jones at 08:31 PM | Comments (0)

[Tech Support] Smart Mailbox limitations in OS X Tiger

First of all, you can't make a smart mailbox for "everyone who is in my address book" Instead, you have to make one for "everyone who is in this group in my address book". So I got around that by making a group for everyone in my address book who does not have an anniversary date set (which is everyone).

But, it turns out that that is not a good solution. Like google, I don't sort, I search. So there's hundreds of messages laying around in my inbox. After a week of this, my "people I know" smart mailbox appears to have given up. It doesnt' even try to list all the messages from people I know. It would appear that the missing option in the smart mailbox config menu hides a performance bug?


Fortunately, disk space is cheap. So the second solution is to create a non-smart mailbox that contains copies of all messages from people in my address book (and not just the trivially univeral group!).

Performance will be better (and has been, so far) on this because each view of my non-smart (dumb?) mailbox does not require a re-query of all the hundreds of messages in my inbox against all of the tens of addresses in my address book. You wonder why they don't cache the results of a query and just rerun it on the new or changed messages after an update. Maybe they do?

The whole thing points out a problem with ALL of the apple-built software I run. And that problem is that apple-built software doesn't deal well with large lists. Xcode (v.1) was useless on a software project with around 50 files and hundreds of classes. Iphoto (the free one) takes a minute or two to open my photo database with 2 thousand photos in it. And now apple mail can't do queries on big message lists.

Posted by jones at 10:43 AM | Comments (0)

May 11, 2005

[Education] David C. Evans Workshop

Held at the Homestead (near Midway Utah) and organized by the BYU EE department. (I was pleasantly surprised to find that the wireless connectivity is good and easy in the conference room we are in. Although the network was pretty flakey, the good news is that there were about 3 networks to switch back and forth between).

Listening to people talk about their teaching was surprisingly interesting, even though most of them teach topics I don't even understand. Quite a few of the speakers clearly spent alot of time thinking critically about how to teach their material. The objectives and content of the courses led to a wide array of creative ideas for teaching a class. The ideas went well beyond the sort of "I spent 10 minutes throwing together some papers the morning classes start" classes that sometimes crop up at the graduate level.

First talk: Harvey Mudd professor David Harris on teaching VLSI.

Second talk: Clint Cole at Digilent. It appears that they are interested in making hardware that students can buy and use in classes. For me, it looks like some very fun toys to buy and put in the lab to see what they can do with them. Their new project on Robotics might be a fun thing to do in an advising seminar with < 10 students.
Erik Brunvand U of U School of Computing VLSI architecture class on designing arithmetic circuits.

I like that circuit design classes take the students through thinking in different levels of abstraction. That's an idea that I'd like to work into my algorithm analysis class, but it may not fit.

Two of the talks brought up this idea of working your time into the design decisions that you make. "If you only have 10 minutes, then just use the built in one" and "if you have the time you might make it faster"

Annette Bunker

Annette Bunker, Utah State U, Teaching formal methods. used the Thomas Kropf book. Wend from BDDs through HOL. That's a long way to go in one semester. Had to go back and pick up DFA.

One page "articulations" on prove to me that you understand this topic that may or may not be in the class.

grading technique called "grade enhancements" if you want a C then you have to do this much... if you want to get a B then you have to do this much... Interesting. For grading, you either get a P+, P or a F. Can resubmit an F until it turns into a P. this iterative grading thing helped quality increase. Feedback was that the grading system was good because they knew where they stood all along. It was hard to get stuff in on time with this grading structure.

All of the 2 (of 7 total) CS students dropped in the first day!

The biggest difference between Annette's class and the one Eric and I teach is that we cover far less material. We just do the core algorithms (symbolic, explicit), theory (automata on infinite words, Kripke Structures) and logics (CTL*, CTL, LTL). We don't read any papers in our first class, but Annette has to do it all in one class.

IEEE Transactions on the Frontiers of Education.

"But I am going to retire, so someone else is going to have to go through this misery"

"I don't care what happens to it, I am retiring"

Chris Myers on teaching. One good assignment is to read this paper, identify the central algorithm code it up and try to duplicate the results. This assignment has come up in some graduate committee meetings I attend. And this assignment may work out well for my 786R class in the fall.

First iteration of the course was a chance to learn what is important in the field. Second time around it was a little clearer what was important, so it was easier to design projects.

Its easier to have them come prepared for a discussion if the class size is small, otherwise they will look stupid in the discussion. Argues well for the oxford style in 786.

Ideas for grading performance: Al Davis make the testing program public with some of the test cases. Publish an anonymous graph with running times from students in the class. To get full credit you have to get within 10% of the best program.

Ideas for presentations on a a class: When you give a talk about a class, well, in Erik's talk about his class, he covered the set projects, some of the outcomes of the open-ended final project. The people who teach classes where the students design a circuit call their supporting tools a "flow" I think calling it a "flow" sort of hints at the idea that this is a large, non-trivial set of tools to support the class.

Talk about the prerequisits you expected, Talk abotu the student population and the purpose of the course in the curriculum (like its the feeder into my research program etc.)

Posted by jones at 01:18 PM | Comments (0)

May 10, 2005

[patents] Design patent for an "ornamental design" for the mac tablet

[United States Patent: D504,889] As reported in various places, Apple has a design patent for a tablet powerBook. Hmm. if it works, I might have to buy one next time I need an office machine.

Posted by jones at 09:41 PM | Comments (2)

May 09, 2005

[Research] Fundamenta Informaticae

[Fundamenta Informaticae] Kevin Seppi, Peter Lamborn and I recently had a paper accepted to this journal. I am thinking about submitting my dissertation work to this journal.

The homepage is kind of hard to find so I thought I would blog it for future reference.

Posted by jones at 10:40 PM | Comments (0)

[Tech Support] CSS Reference

CSS Tutorial Its meant to be a tutorial but it has key and value lists that I find quite useful. When working on my Logics Webpage with students in an independent study class.

Posted by jones at 02:51 PM | Comments (0)

[Research] Thesis topic ideas

These are some thesis topic ideas I chanced upon while working on a proposal.


Posted by jones at 11:13 AM | Comments (1)

May 04, 2005

[Tech Support] Mac OS X 10.4 Tiger Install and First Impressions

[Google Search: os x tiger ] I did the "archive my system directory and save my accounts" installation on a powerbook G4 with 1.2ish GB of RAM on an 80 gig hard drive and "only" 17 gigs of free space.

Install

The interface for setting up the installation options is terrible. The "archive my stuff and save my account option" is an option under "customize" on the screen where you pick which drive to install to. I had to open the printed instructions to figure it out. Embarrasing.

Setup took 41 mins 11 secs, it was 43 mins 1 sec from "reboot to install" to first login screen. Install would have taken about 10 minutes less to do the install if I didn't install ALL of the language support. But I guess I can sleep better at night knowing that my Norwegian friends can use my laptop assuming they need it and can't do it in English and that I meet some Norwegian people and they want to be my friend and they need a laptop. Anyway, its done.

It took 1 hour 29 mins for Spotlight to index my hard drive.

First impressions

The look and feel is pretty much unchanged. There's still no cool screensavers or background images. c'est la vie.

Spotlight is cooler than I thought it would be. I thought I would be sad because it won't search my mail messages in Entourage, but...

The new Mail.app is actually usable, so I don't need entourage anymore. The smart folders are fun, search is actually usable (it wasn't on the old mail) and I am happy with it. I don't have worry about that lingering fear that my extremely un-portable and un-fixable Entourage database will die.

At first the RSS aggregator in Safari looked useless. It appeared that it wouldn't aggregate and it wouldn't show my un-viewed message counts on the bookmark bar. But, a quick read of the apple web page on the new safari and some poking around by two CS professors (it would have been faster for almost anyone else to figure it out) we found that you can aggregate feeds by...


  1. Put all the feeds you want to aggregate in a folder in your bookmarks
  2. drag that folder into your bookmarks bar.
  3. click on the folder name
  4. in the drop down menu, select "view all RSS articles"
  5. drag the location of that page into the bookmark bar
  6. voila, you have a book mark for all the feeds in that folder.
  7. un-viewed article count appears next to the feed name in the bookmark bar.

If there's an easier way, I'd like to hear about it.

The dashboard stuff is way over the top. I mean, I see the value and its cool (but I thought expose was cool the first day and haven't used it since) but the ripple effects and the slow turning over effect are just gratuitous iCandy. We'll see if it drops into the gimmick category in a few more days.

emacs didn't work.

CodeTek Virtual desktop pro didnt' work.

Fire didn't work (but I just need to download the next version and it will)

Everything else is humming along just fine. Surprisingly painless overall.

Posted by jones at 09:38 PM | Comments (0)