« May 2005 | Main | July 2005 »

June 29, 2005

[Research] Low level BIR syntax

[2.13. Low-level Thread or Function Body] Useful to know for writing a BIR transition to BDD translator. Helpfully linked to javadoc sources for the Bogor AST class.

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

June 24, 2005

[Education] My take on writing an MS Thesis Proposal at BYU

As a young academic, I am somewhat obligated to form an opinion on "how things should be done" and promulgate that opinion free of charge to others. Here is what I think an MS Proposal should be like and some thoughts on what the proposal presentation should look like.

There are also some examples in the same directory.

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

June 23, 2005

[Education] What Algorithm Does nuSMV Use?

[The mc package for maintainers] Its an interesting question and it looks like the answer is that one would start with the set of states that do (or don't) satisfy a property and then apply the transition relation forwards (or backwards) to compute the set of states reachable from (or in the preimage of) the starting states.

The point here is to figure out which way to teach it in CS 586 (introduction to model checking) at BYU.

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

[Misc.] Getting lost on my morning commute.

My bicycling commute Tuesday included a ride up the Bonneville shorline trail from 800 north in Orem to the north side of Provo Canyon then down into the Provo Canyon Race loop trail then finally to BYU campus. It was a 12 mile ride. The best part (other than the single track) was getting lost on the way to work. That Provo Canyon race loop is confusing! I've worked at BYU for 3.5 years now and it was good to change up the commute and get lost .

I went back this morning to figure out where I was and still couldn't figure it out. But it was also a good ride.

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

June 17, 2005

[Research] Integrating Bogor and JavaBDD

The goal here is to be able to use off-the-shelf BDD libraries through the JavaBDD interface in Bogor. I am an Eclipse novice, so this will be a rather pedantic description of what I did.


  1. Obtain and unzip a copy of the JavaBDD-src distribution. Put it in a directory and remember where you put it.
  2. right click on your Bogor project in eclipse (see previous post on how to do that).
  3. Select "Build path" then "link additional source to project"
  4. Navigate your way to the unzipped directory from step 1.
  5. Click ok etc until done.
  6. JavaBDD requires the BDD libraries, lib(buddy|cal|cudd).jnilib, to be on the java.library.path. My solution was to simply copy the libraries to /usr/lib/java. That worked great. See Eclipse Plugin Central for pointers on working with java.library.path.

Next, test the thing and make sure all is well.

  1. test 1: can I run the JavaBDD n-queens example? In the "default package" of my newly created javaBDD directory in my bogor project, I right click on NQueens.java and select "run as" then "run ..."
  2. Under "arguements" I type in "5" for program arguements then run it.
  3. about 0.537 seconds of program execution time later, the program has terminated with a solution
  4. test 2

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

    June 14, 2005

    [Misc.] Repairing a Canon PowerShot

    [IXUS-World (alles zur Canon IXUS 700, IXUS 50, IXUS 40, IXUS 30, IXUS i5, IXUS 500, IXUS 430 IXUS, IXUS IIs, IXUS i, IXUS II, IXUS 400, IXUS V3, IXUS V2, IXUS 330, IXUS V, IXUS 300 und Ur-IXUS)] My camera died an untimely death at scout camp last week. It looks like I may be able to repair it at home though. I am about done with part 1. So far so good!

    Posted by jones at 08:46 AM | Comments (0)

    June 02, 2005

    [Research] Yet another low-level mc68hc11 reference

    [Mikrocomputertechnik] Lists many of the soft registers and what each bit means. Indexed by address, which is handy if you are reading straight assembly code.

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

    [Misc.] Quest Sues over UTOPIA

    [Phil Windley's Technometria | Qwest Files Suit to Block UTOPIA] I found this on Phil's blog. As an Orem resident, this is an important issue for me. I should confess that I don't understand the business and governmental issues here, but as a faithful Qwest bill-payer (I have phone and DSL through qwest), I am very excited to pay UTOPIA less than I currently pay qwest but to get more bandwidth!

    If Qwest feels threatened by UTOPIA, which they probably should, then maybe Qwest should get busy and get fiber to my house. Qwest might also consider reviewing their pricing structure and determine if they are competitive in a competitive free market economy.

    I would guess that Qwest will argue that the governments have an unfair advantage. I don't know the answer to that question, but from where I am sitting, Qwest looks like an expensive monopoly that's not innovating on my behalf. I am happy to have my government intervene here.

    Posted by jones at 11:57 AM | Comments (0)

    [Research] Ada language reference

    [Programming:Ada - Wikibooks] In an effort to demonstrate that our language-independent software model checker, called Estes, is indeed landuage independent, I am writing and verifying a little Ada program. That would of course be easier if I actually knew how to write Ada. Interestingly, this brings me full-circle in a way. I got into CS because my Dad was (and still is) in CS. My Dad did a ton of Ada work as an Air Force officer. So I suppose I can always ask him for help if/when I get stuck.

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