NuSMV

Today I have installed NuSMV, which is one of the SMV model checker.

SMV, Simbol Model Verification, is a famous Model checking way.

Professor. Ammann gave students an assignment which I have to grade next week.
The assignment was about SMV which I don't have enough knowledge.

I have heard SMV can represent finite automata.
It is very interesting that somebody made a tool that we can use freely.
There are several SMV checkers and NuSMV is one of them: Cadence SMV, VCEGAR.

For a backup, I refer professor's example here:

-- SMV Specification for simple EW,NS intersection
-- Paul Ammann

MODULE main
VAR
EW       : direction; NS : direction;

EWGreen  : process ToGreen(EW, NS);
NSGreen  : process ToGreen(NS, EW);

EWYellow : process ToYellow(EW);
NSYellow : process ToYellow(NS);

EWRed    : process ToRed(EW);
NSRed    : process ToRed(NS);

--ASSIGN

-- (EW, NS) check for P1
SPEC
 AG((EW.light = red | NS.light = red))
SPEC
 AG((NS.light = green ) -> AX (EW.light = red))

-- spec for test generation
--SPEC
--   AG((NS.light = green ) -> (AG !(NS.light = red)))


MODULE direction
VAR
 light : {red, yellow, green};
ASSIGN
 init(light) := red;

MODULE ToGreen(dir1, cdir1)

ASSIGN
 next(dir1.light) :=
    case
     (dir1.light = red) & (cdir1.light = red) : green;
     1 : dir1.light;
    esac;

MODULE ToYellow(dir1)

ASSIGN
 next(dir1.light) :=
    case
     (dir1.light = green) : yellow;
     1 : dir1.light;
    esac;

MODULE ToRed(dir1)

ASSIGN
 next(dir1.light) :=
    case
     (dir1.light = yellow) : red;
     1 : dir1.light;
    esac;

This seems complex, but it will be very powerful if we can have formal specification using these kind of Model Checking.

Adeona - LoJack for laptop

BB told me a interesting free software: Adeona.
http://adeona.cs.washington.eduThis program is for the case that your laptop is stolen.
This software periodically run on background, gather network information and give you some hints where your laptop is.

The website recommend you do *not* try to catch the thief by yourself even when you find out where it is.

One interesting thing is the software can take a picture of the thief when your computer is MacBook series, which has a camera at top of the LCD.

The logic was simple, so that I made similar one by myself.Using my shell program will get some network information and picture file onto your email box every half hour; you may be able to use some "filters" for the spam-like emails.In order to use this, you need to set your email address on the script file, "email", and install two software: iSightCapture, mutt.
I don't know which way is easiest way to install mutt, but I used "Mac Port".

You can add a schedule onto your "crontab" like this:

0,30 * * * * /Users/wrice/Applications/sendPicture.sh

Enjoy your safer environment.

Game Maker 7

I haven't heard about this before today.
There is a game making tool called "Game Maker."
The recent version is 7 now.
It is free to download.You can see 100 games that are made by the tool in you tube.
100 Game Maker games in 10 minutes.

The movie clip inspires me a lot of new ideas for game design.
And it is also surprising that a game tool is that much flexible.

The tendency of the profit ratio to fall

One of Korean economy professor, SungJin Jung, claimed that the profit ratio in America industry has tendency of the ratio of profit to fall, which is one of the famous Marx's theory.
In his article he was using America government data, which is open data to public.

The diagram he was using is here:The data is from one of the government web site: http://www.bea.gov
Non- financial corporate sector ratio = National Income and Product Accounts, Table 1.14. line 24(net operating surplus)-line 26 (business current transfer payment) / Fixed Asset Table, Table 4.1. line 28(non-financial)

Considering the non-financial corporate sector ratio as profit ratio, the point of this article is that the diagram indicates the profit ratio has tendency to fall.

I wanted to get the diagram by myself, so I made it; this means everybody can draw the diagram.
There is two reason why the diagrams are different.
One is that the web site revised the data after the article is written. The other reason is that I included two more years: 2006, and 2007. And the government web site doesn't have data before 1930.
You can see the Trend line is declining.

I, however, found one interesting point.
Two of them averaging the data by 5 years.
But if I just use raw data, which is year by year, then I get different diagram here:
If you click the diagram above, you can see bigger one.
The new line looks like *flat*, not declining.
The reason is the new diagram is wider.
If I make it narrow, then you can see the same declining line like this:
In brief, although different analysis way shows different diagram, it is definitely not increasing. It is opposite result from the opinions of some of famous leftists who claims that the falling tendency problem is overcame.

In addition, even though we can say it is declining, it does not look significant.