Adding Spin support to CSight.

ModelInference / synoptic

Inferring models of systems from observations of their behavior

Other

81 stars 25 forks source link

Adding Spin support to CSight. #374

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago

Why is this enhancement useful?
This is a step in implementing issue 278.

SPIN is a model checker that supports bounded queues.

SPIN takes a Promela representation of a model as input, so I need to convert 
CSight's internal representation of the model to properly formatted Promela.

What is an example use case for this enhancement?

There's shouldn't be an explicitly visible use to the user at this point. This 
is more of an internal enhancement.

Original issue reported on code.google.com by Kenneth....@gmail.com on 28 May 2014 at 1:59

Blocking: #375, #376

GoogleCodeExporter commented 9 years ago

Original comment by Kenneth....@gmail.com on 5 Jun 2014 at 11:49

Now blocking: #375

GoogleCodeExporter commented 9 years ago

Issue 375 has been merged into this issue.

Original comment by Kenneth....@gmail.com on 3 Jul 2014 at 5:19

GoogleCodeExporter commented 9 years ago

This includes the full Spin model checking support. 

Solution in revision 12ade639f32aca579daa868dcfce3ba9a70e4e97, please review.

Original comment by Kenneth....@gmail.com on 3 Jul 2014 at 5:31

Changed title: Adding Spin support to CSight.

GoogleCodeExporter commented 9 years ago

Original comment by Kenneth....@gmail.com on 4 Jul 2014 at 3:30

Now blocking: #376

GoogleCodeExporter commented 9 years ago

Basic optimizations have been added to CSight.

Solution in revision 0e15e4d2708ca970f66ebff98fbfef113a619380, please review.

Original comment by Kenneth....@gmail.com on 10 Jul 2014 at 6:20

GoogleCodeExporter commented 9 years ago

Merged into default with revision bc174bec0bcb

Original comment by bestchai on 14 Jul 2014 at 5:12

Changed state: Fixed