Code gen

[xiaohe27]

@grosu @kheradmand
This is the beta version of RV-Monitor in K.
Given an rvm spec using FSM properties, it is able to generate monitoring library in C.

Currently, only FSM plugin is supported, and one rvm spec file is supported.

In the generated code, some unnecessary assignments exist (these junks do not affect the correctness though, can be removed later).

In the limited tests, it is able to generate C monitoring code correctly for the spec which contains multiple FSM formulas (In terms of the C monitoring code generation function, in the current RV-Monitor which is written in java, only the first FSM formula will be handled and transformed to C monitoring code).

I used the benchmark 'SeatBelt' from RV-Monitor's repository, I modified the makefile so that it is building and testing the rv-monitor implemented in K. The benchmark is in the location:

rvm-parser/test/rvm/fsm/rvc/SeatBelt

In that directory, do the following to see the effects:

1. make all
2. make test

For this test, the monitoring code generated by rv-monitor-in-k behaves the same as the original rv-monitor-in-java w.r.t. the output.

@kheradmand I also modified some syntax you defined at some points to ease the process of writing rules and removing ambiguities.