fleet

Editor GitHub mit-zardini-lablibraries act4brd specs models thingsfleet
Editor
Visualization
mcdp { provides composition [`fleet] requires total_capital_cost [USD] requires total_num_operators [Nat] dp_t1 = instance `fleet_type_1 dp_t2 = instance `fleet_type_2 dp_fleet_trival = instance `fleet_trival required total_capital_cost >= capital_cost required by dp_t1 + capital_cost required by dp_t2 required total_num_operators >= operators required by dp_t1 + operators required by dp_t2 provided composition <= composition provided by dp_fleet_trival number_t1 required by dp_fleet_trival <= number_t1 provided by dp_t1 number_t2 required by dp_fleet_trival <= number_t2 provided by dp_t2 }
Diagramremove
Other informationremove
Internal representation details
CompositeNDP                                                                                                                                              
│    provides   composition   Fin {fleet_0_2,fleet_0_3,fleet_1_1,fleet_1_2, …} │ requires   total_capital_cost    SB(≥0) USD                              
│                                                                              │ requires   total_num_operators   SB(≥0::1)                               
│  8 nodes, 9 edges                                                                                                                                       
│   connected rec: ✓                                                                                                                                      
│  provided composition                  ≤ composition provided by dp_fleet_trival   equiv id                                                             
│  _result required by _sum              ≤ required total_capital_cost               equiv id                                                             
│  _result2 required by _sum1            ≤ required total_num_operators              equiv id                                                             
│  number_t1 required by dp_fleet_trival ≤ number_t1 provided by dp_t1               diff  AmbientConversion SB({0, 1, 2, 3}) car  ⇸  SB(≥0) car  > D car 
│                                                                                           𝒇 ≤ 𝒓                                                         
│  number_t2 required by dp_fleet_trival ≤ number_t2 provided by dp_t2               diff  AmbientConversion SB({0, 1, 2, 3}) car  ⇸  SB(≥0) car  > D car 
│                                                                                           𝒇 ≤ 𝒓                                                         
│  capital_cost required by dp_t1        ≤ dp_t1_capital_cost provided by _sum       equiv id                                                             
│  operators required by dp_t1           ≤ dp_t1_operators provided by _sum1         equiv id                                                             
│  capital_cost required by dp_t2        ≤ dp_t2_capital_cost provided by _sum       equiv id                                                             
│  operators required by dp_t2           ≤ dp_t2_operators provided by _sum1         equiv id                                                             
├            _sum: SimpleWrap                                                                                                                             
│                  │  provides   dp_t1_capital_cost   SB(≥0) USD │ requires   _result   SB(≥0) USD                                                        
│                  │  provides   dp_t2_capital_cost   SB(≥0) USD │                                                                                        
│                  └ M_Res_AddMany_DP SB(≥0)×SB(≥0) ⟨USD,USD⟩  ⇸  SB(≥0) USD                                                                              
│                     𝒇₁ + 𝒇₂ ≤ 𝒓                                                                                                                         
│                    ├      Fs: ├ SB(≥0) USD                                                                                                              
│                    │          └ SB(≥0) USD                                                                                                              
│                    ├ opspace: SB(≥0) USD                                                                                                                
│                    └    algo: ApproximationAlgorithms - ApproximationAlgorithms.VAN_DER_CORPUT                                                          
├           _sum1: SimpleWrap                                                                                                                             
│                  │  provides   dp_t1_operators   SB(≥0::1) │ requires   _result2   SB(≥0::1)                                                            
│                  │  provides   dp_t2_operators   SB(≥0::1) │                                                                                            
│                  └ M_Res_AddMany_DP WU ⟨dimensionless,dimensionless⟩  ⇸  SB(≥0::1)                                                                      
│                                     └ Π<2>                                                                                                              
│                                       ├ SB(≥0::1)                                                                                                       
│                                       └ SB(≥0::1)                                                                                                       
│                     𝒇₁ + 𝒇₂ ≤ 𝒓                                                                                                                         
│                    ├      Fs: ├ SB(≥0::1)                                                                                                               
│                    │          └ SB(≥0::1)                                                                                                               
│                    ├ opspace: SB(≥0::1)                                                                                                                 
│                    └    algo: ApproximationAlgorithms - ApproximationAlgorithms.VAN_DER_CORPUT                                                          
├ dp_fleet_trival: SimpleWrap                                                                                                                             
│                  │  provides   composition   Fin {fleet_0_2,fleet_0_3,fleet_1_1,fleet_1_2, …} │ requires   number_t1   SB({0, 1, 2, 3}) car             
│                  │                                                                            │ requires   number_t2   SB({0, 1, 2, 3}) car             
│                  └ DP_Catalog Fin {fleet_0_2,fleet_0_3,     ⇸  WU ⟨car,car⟩                                                                             
│                                    fleet_1_1,fleet_1_2, …}     └ Π<2>                Showing first 5 of 7                                               
│                                                                  ├ SB({0, 1, 2, 3})  fleet_1_1  ↤  modelsub1  ↦  ⟨1 car,1 car⟩                          
│                                                                  └ SB({0, 1, 2, 3})  fleet_2_0  ↤  modelsub2  ↦  ⟨2 car,0 car⟩                          
│                     catalogue(𝒇, 𝒓)                                                  fleet_0_2  ↤  modelsub3  ↦  ⟨0 car,2 car⟩                          
│                                                                                      fleet_2_1  ↤  modelsub4  ↦  ⟨2 car,1 car⟩                          
│                                                                                      fleet_1_2  ↤  modelsub5  ↦  ⟨1 car,2 car⟩                          
├           dp_t1: CompositeNDP                                                                                                                           
│                  │    provides   number_t1   SB(≥0) car │ requires   capital_cost   SB(≥0) USD                                                          
│                  │                                      │ requires   operators      SB(≥0::1)                                                           
│                  │  5 nodes, 4 edges                                                                                                                    
│                  │   connected rec: ✓                                                                                                                   
│                  │  provided number_t1       ≤ _op provided by _mult    equiv id                                                                        
│                  │  provided number_t1       ≤ _op provided by _mult1   equiv id                                                                        
│                  │  _res required by _mult   ≤ required capital_cost    equiv id                                                                        
│                  │  _res2 required by _mult1 ≤ required operators       diff  AmbientConversion SB(≥0)  ⇸  SB(≥0::1)  > D                               
│                  │                                                             𝒇 ≤ 𝒓                                                                    
│                  ├  _mult: SimpleWrap                                                                                                                   
│                  │         │  provides   _op   SB(≥0) car │ requires   _res   SB(≥0) USD                                                                
│                  │         └ DP_L_UME SB(≥0) car  ⇸  SB(≥0) USD                                                                                         
│                  │            𝒇 ⋅ 1200000 ≤ 𝒓                                                                                                           
│                  │           M_C_WrapUnits   car → USD > M_A_Mult1_Upper   SB(≥0)  →   same x ⟼ x ⋅ 1200000                                             
│                  └ _mult1: SimpleWrap                                                                                                                   
│                            │  provides   _op   SB(≥0) car │ requires   _res2   SB(≥0)                                                                   
│                            └ DP_L_UME SB(≥0) car  ⇸  SB(≥0)                                                                                             
│                               𝒇 ≤ 𝒓                                                                                                                     
│                              M_C_WrapUnits   car → dimensionless > M_Identity   SB(≥0)  →   same x ⟼ x                                                  
└           dp_t2: CompositeNDP                                                                                                                           
                   │    provides   number_t2   SB(≥0) car │ requires   capital_cost   SB(≥0) USD                                                          
                   │                                      │ requires   operators      SB(≥0::1)                                                           
                   │  5 nodes, 4 edges                                                                                                                    
                   │   connected rec: ✓                                                                                                                   
                   │  provided number_t2       ≤ _op provided by _mult    equiv id                                                                        
                   │  provided number_t2       ≤ _op provided by _mult1   equiv id                                                                        
                   │  _res required by _mult   ≤ required capital_cost    equiv id                                                                        
                   │  _res2 required by _mult1 ≤ required operators       diff  AmbientConversion SB(≥0)  ⇸  SB(≥0::1)  > D                               
                   │                                                             𝒇 ≤ 𝒓                                                                    
                   ├  _mult: SimpleWrap                                                                                                                   
                   │         │  provides   _op   SB(≥0) car │ requires   _res   SB(≥0) USD                                                                
                   │         └ DP_L_UME SB(≥0) car  ⇸  SB(≥0) USD                                                                                         
                   │            𝒇 ⋅ 850000 ≤ 𝒓                                                                                                            
                   │           M_C_WrapUnits   car → USD > M_A_Mult1_Upper   SB(≥0)  →   same x ⟼ x ⋅ 850000                                              
                   └ _mult1: SimpleWrap                                                                                                                   
                             │  provides   _op   SB(≥0) car │ requires   _res2   SB(≥0)                                                                   
                             └ DP_L_UME SB(≥0) car  ⇸  SB(≥0)                                                                                             
                                𝒇 ≤ 𝒓                                                                                                                     
                               M_C_WrapUnits   car → dimensionless > M_Identity   SB(≥0)  →   same x ⟼ x