Add ability to constrain steps

[pxlcoder]

A list of constraints can now be specified alongside the step command, enabling the user to specify paths of execution. The length of the list represents the number of transitions, and the i-th element of the list is the constraint applied to the i-th transition.

If an empty string is specified as a constraint at a particular index, no constraint will be applied to the corresponding transition.

This functionality is implemented by creating an auxiliary predicate for each constraint. After these predicates have been created, a master path predicate is generated, containing a conjunction of the auxiliary predicates. Finally, the run command calls path[first] to apply the master predicate beginning at the first state.

Usage example:

(aldb) load models/river_crossing.als
Reading model from models/river_crossing.als...done.
(aldb) step ["Chicken in far"]

S2
----
far: { Chicken, Farmer }
near: { Fox, Grain }

(aldb) step ["", "far=Chicken+Farmer+Grain"]

S4
----
far: { Chicken, Farmer, Grain }
near: { Fox }

(aldb) history

(-3)
----
S1
----
far: {  }
near: { Chicken, Farmer, Fox, Grain }

(-2)
----
S2
----
far: { Chicken, Farmer }
near: { Fox, Grain }

(-1)
----
S3
----
far: { Chicken }
near: { Farmer, Fox, Grain }

Closes #17.

[liangdrew]

I don't think we need to print out the current state again if a constraint is unsatisfiable:

(aldb) current

S1
----
far: {  }
near: { Chicken, Farmer, Fox, Grain }

(aldb) step [Chicken=far]
Cannot perform step. Transition constraint is unsatisfiable.

S1
----
far: {  }
near: { Chicken, Farmer, Fox, Grain }

(aldb)

[aman-dureja]

You should be more clear that the user can either specify the number of steps or a list of constraints. Something like: "Instead of a numeric number of steps, step constraints may be specified as a comma-separated list enclosed in square brackets."

[aman-dureja]

Code looks good. Please manually test it with the musical chairs model before merging; that model is more complex than RCP and is useful for exposing potential bugs.