Issues with Verify() function

[dassarthak18]

We are currently modeling a hybrid automaton in Verse to achieve clock synchronization in swarm robotic systems. The simulate_simple() function works as expected. However, we are facing the following error while trying to call verify().

`[(<RobotMode.Wait: 1>,), (<RobotMode.Wait: 1>,), (<RobotMode.Wait: 1>,), (<RobotMode.Wait: 1>,), (<RobotMode.Wait: 1>,)] <class 'list'> {'robot_1': ['Wait'], 'robot_2': ['Wait'], 'robot_3': ['Wait'], 'robot_4': ['Wait'], 'robot_5': ['Wait']} Traceback (most recent call last): File "/home/sarthak/Verse-library-main/demo/robot_swarm.py", line 53, in traces = swarm.verify(10, 0.01) File "/home/sarthak/Verse-library-main/verse/scenario/scenario.py", line 353, in verify tree = self.verifier.compute_full_reachtube(init_list, init_mode_list, static_list, uncertain_param_list, agent_list, self, time_horizon, File "/home/sarthak/Verse-library-main/verse/analysis/verifier.py", line 244, in compute_full_reachtube asserts, all_possible_transitions = transition_graph.get_transition_verify(new_cache, paths_to_sim, node) File "/home/sarthak/Verse-library-main/verse/scenario/scenario.py", line 850, in get_transition_verify if dest_track == track_map.h(src_track, src_mode, dest_mode): File "/home/sarthak/Verse-library-main/verse/map/lane_map.py", line 119, in h return self.h_dict[(lane_idx, agent_mode_src, agent_mode_dest)] KeyError: ('', 'Wait', 'Wait')

Please find attached the python file for our model here.

[lyg1597]

Hi, Sorry for the late response. We looked into the problem you encountered. I think the major cause of this problem is that the map you are using doesn't match the decision logic you are using. Since you are not using the map in this scenario, you shouldn't specify any exisiting map. The modified model files are attached here. The model file should work with the latest code on the main branch.

[dassarthak18]

Hi, Could you please explain the reason behind the modifications in the decisionLogic of the agent, particularly the reason for adding an FLMode? Also, the verification routine in the modified model files is taking too long even for a time horizon of 10.

[lyg1597]

For the FLMode part it's mainly a modeling technique. As in this example, the flmode variable is mainly an integer valued variable which can only take values 0 and 1, it would be better to treat it as a discrete variable, which can be encoded as FLMode. I think for me the verification routine can finish in around 2minutes. Please pull the most recent code on the main branch for this example.

[dassarthak18]

I pulled the most recent code on the main branch. Verification is working as expected. Thanks!