ml4ai/funman

SKEMA Functional Model Analysis (FUNMAN)

funman's Issues

Move all utils to a utils subdir

Move all utils to a utils subdir

Develop FastAPI

Update documented use cases

1. Single shot solver: consistency, parameter synthesis
2. Comparison: cross-model, and model-sim
3. Visualization/Analysis

Development steps:

• examples/ version of each
• pytest
• documentation
• notebook

Update documentation against reorganized code for release 1.3

Precommit hooks

1. black
2. tests (for merging)
3. debug statements
4. reorder imports

Factor out parameter space processing

The following logic occurs in many places and make some changes more effort than they should be. Perhaps go through and factor out those uses into so shared function call.

inst = ParameterSpace.decode_labeled_object(data)                                                                                                                        
label = inst.label                                                                                                                                                           
if isinstance(inst, Box):                                                                                                                                                    
    if label == "true":                                                                                                                                                      
        true_boxes.append(inst)                                                                                                                                              
    elif label == "false":                                                                                                                                                   
        false_boxes.append(inst)                                                                                                                                             
    else:                                                                                                                                                                    
        l.info(f"Skipping Box with label: {label}")                                                                                                                          
elif isinstance(inst, Point):                                                                                                                                                
    if label == "true":                                                                                                                                                      
        true_points.append(inst)                                                                                                                                             
    elif label == "false":                                                                                                                                                   
        false_points.append(inst)                                                                                                                                            
    else:                                                                                                                                                                    
        l.info(f"Skipping Point with label: {label}")                                                                                                                        
else:                                                                                                                                                                        
    l.error(f"Skipping invalid object type: {type(inst)}")

Move all utils to a utils subdir

Add code coverage tool

Remove unused DrealBoxSearch

Create Symbol class to encapsulate strings and model identifiers

Move parameter space point analysis to parameter space from parameter synthesis result.

Ensure API level intervals take precedence over model intervals

Docker builds

Containers:

• Dev
• Demo
• dreal build (common parent of the above)

Steps:

1. Fix Dockerfile.dreal4 to build cleanly
2. Remove Dockerfile.dev, use Dockerfile only
3. Demo container uses pypi instead of local install.

New tests

• Single process box search
• math utils
• representation coverage

Create SEIRD AMR model

Cleanup tests for petri and regnet models

There are several temp tests marked for skipping that can likely be removed or converted into more permanent tests.

The regnet test also contains a test that should be enabled but is currently too slow. That test should be revisited and enabled.

try/except import funman_dreal with error message

See funman.search_utils.py:946

Move funman.model.bilayer.to_smtlib() translation to model2smtlib

Update FUNMAN API

Modify the API to consolidate Consistency and ParameterSynthesis scenarios as follows:

• Input:
  • Model (json)
  • Parameters (ranges and any/all flag to indicate if synthesized)
  • Query (list of constraints)
    • Start with bounds on state variables
    • Next steps: revisit demo/eval constraints for inclusion

Consolidate Test cases

Minimum requirements:

• Models: hand coded, bilayer, petrinet to bilayer
• Scenarios: consistency, parameter synth
• Parameter spaces: consolidate
• Move to scratch: incremental solve, smtlib writing,
• Keep: cached parameter spaces,

Default move everything to scratch and pull back what we want.

Create funman.search subdir

Separate different search implementations to different files.

Convert model2smtlib to an aux package

API

• define standalone interface that includes directives, and calls funman functions.
• not sure if should be sub package or aux package.
• funman package should not depend on API.

Process Metadata from bilayer and use to encode variable bounds.

Create funman.search subdir

Separate different search implementations to different files.

Consolidate search._run_handler and search._run_handler_step

Move funman.examples to funman_demo

Add json input can jsonschema

Consolidate search._run_handler and search._run_handler_step

Revisit notebooks and auxiliary packages.

• Document auxiliary packages and bring into RTDs
• Update auxiliary tests and notebooks
• Update main notebooks.

Add petri net ingest unit test to scratch

Test Issue

Add thin thread petrinet modelsupport

Add support for petrinet model format to the generalized encoding branch changes (after they get merged)

Add time key to parameters

Check whether the Terrarium syntax for time dependent parameters would be a better representation. Otherwise, parameters are of the form:

{
  "name": "beta",
  "lb": 0.1,
  "ub": 0.2,
  "time": 22
  "label": "any"
}