another example (cardiac cell)

demo/fp_demos/buckling_col.py

@@ -19,7 +19,6 @@
 
 from verse.utils.fixed_points import *
 from verse.analysis.verifier import ReachabilityMethod
-from z3 import *
 from verse.stars.starset import *
 
 from verse.sensor.base_sensor_stars import *

demo/fp_demos/cardiac_cell_demo.py

@@ -11,7 +11,10 @@
 
 from z3 import *
 from verse.utils.fixed_points import *
+from verse.analysis.verifier import ReachabilityMethod
+from verse.stars.starset import *
 
+from verse.sensor.base_sensor_stars import *
 
 if __name__ == "__main__":
 
@@ -22,23 +25,37 @@
 
     scenario = Scenario(ScenarioConfig(init_seg_length=1, parallel=False))
 
-    scenario.add_agent(cell) ### need to add breakpoint around here to check decision_logic of agents
+    # scenario.add_agent(cell) ### need to add breakpoint around here to check decision_logic of agents
 
-    init_cell = [[0, 0], [0, 0]]
-    # # -----------------------------------------
+    # init_cell = [[0, 0], [0, 0]]
+
+    basis = np.array([[0, 0], [0, 0]]) * np.diag([0.05, 0.05]) 
+    center = np.array([0,0])
+    C = np.transpose(np.array([[1,-1,0,0],[0,0,1,-1]]))
+    g = np.array([1,1,1,1])
 
-    scenario.set_init_single(
-        'cell', init_cell,(CellMode.On,)
+    cell.set_initial(
+        StarSet(center, basis, C, g),
+        tuple([CellMode.On])
     )
+    # # -----------------------------------------
 
-    trace = scenario.verify(30, 0.01)
+    # scenario.set_init_single(
+    #     'cell', init_cell,(CellMode.On,)
+    # )
+    scenario.add_agent(cell)
+    scenario.config.reachability_method = ReachabilityMethod.STAR_SETS
+    # scenario.config.pca = False
+    scenario.set_sensor(BaseStarSensor())
+    trace = scenario.verify(5, 0.1)
     # sim = scenario.simulate(10, 0.01)
     # pp_fix(reach_at_fix(trace, 0, 10))
-    print(f'Fixed points exists? {fixed_points_fix(trace, 30, 0.01)}')
-
-    fig = go.Figure()
-    fig = reachtube_tree(trace, None, fig, 0, 1, [0, 1], "fill", "trace")
-    fig = reachtube_tree_slice(trace, None, fig, 0, 1, [0, 1], "fill", "trace", plot_color=colors[1:])
 
+    stars = []
+    for star in trace.nodes[0].trace['cell']:
+        stars.append(star[1])
+    plot_stars_points(stars)
+    print(stars[-1].basis[0][0])
+    plot_reachtube_stars(stars)
     # fig = simulation_tree(trace, None, fig, 1, 2, [1, 2], "fill", "trace")
-    fig.show()
+    plt.show()