State Exploration Multithreading

[ifndefJOSH]

Part of the improvements for STAMINA 2.5 involve asynchronous multithreaded exploration of states by multiple threads as requested by the user. Commit c099b02 creates skeleton for this, but I have a couple of ideas/concerns.

• Should the threads be in their own namespace?
• Should they be in the same file as the builders?

[ifndefJOSH]

Progress report:

• Added lockable queue
• Added thread skeleton
• Added template for implementation

[ifndefJOSH]

Progress report:

• Added -j option. (464a332)
• Debugged templating order issue with *Thread classes
• Working on changing StateType to StateAndThreadIndex where necessary
• Removed unnecessary remapping method (9ac4e94)

[ifndefJOSH]

The thread index is stored in an instantiation of storm::storage::sparse::StateStorage<stamina::builder::threads::ControlThread::StateAndThreadIndex<StateType>> but the builder class requires the StateStorage<> to be templated with just StateType. Not sure how to resolve this. Should I

1. Use two BitVectorHashmaps?
2. Try to figure out a way to force the generator to take the state storage

[ifndefJOSH]

An additional idea:

Create two classes:

• One which inherits from storm::storage::sparse::StateStorage
• One which inherits from storm::storage::BitVectorHashMap

Which will also store the thread values, rather than having a StateAndThreadIndex

[ifndefJOSH]

Other idea to add:

State ownership "expires" based on a LRU cache policy so the owned states hashmap will be a fixed size and thread ownership will be more even. This reduces the need for defragmentation.