one

Editor GitHub co-design-modelslibraries drawings specs models thingsone
Editor
Visualization
mcdp { provides f₁[m] provides f₂[m] requires r₀[m] provided f₁ + 10 cm ≤ 10 m provides x[m] requires y[m] provided x ≤ required y provided f₁ + provided f₂ ≤ required r₀ provided x ≤ 100 m a = instance mcdp { provides ff[m] requires ff = provided ff · 2 requires x[m] required x ≥ 1 m } requires x for a # x required by a ≼ ff provided by a provides ff using a requires ff for a }
Diagramremove
Other informationremove
Internal representation details
CompositeNDP                                                                                          
│    provides   f_1   SB(≥0) m      │ requires   r_0   SB(≥0) m                                       
│    provides   f_2   SB(≥0) m      │ requires   y     SB([0,100]) m                                  
│    provides   x     SB([0,100]) m │ requires   x     {1 m}                                          
│    provides   ff    SB(≥0) m      │ requires   ff    SB(≥0) m                                       
│  13 nodes, 10 edges                                                                                 
│   connected rec: ✓                                                                                  
│  provided f_1             ≤ _op provided by _plus   equiv id                                        
│  provided f_1             ≤ f_1 provided by _sum    equiv id                                        
│  provided f_2             ≤ f_2 provided by _sum    equiv id                                        
│  provided ff              ≤ ff provided by a        equiv id                                        
│  provided x               ≤ _l1 provided by _lim1   diff  (always satisfied)                        
│  provided x               ≤ required y              equiv id                                        
│  _res required by _plus   ≤ _l provided by _lim     diff  DP_GenericConstant SB(≥0.1) m  ⇸  {10 m}  
│                                                            𝒇 ≤ 10 m                                 
│                                                           ├  b: ()                                  
│                                                           ├ lf: LowerSet(maximals=ff❨10.000000000❩) 
│                                                           └ ur: UpperSet(minimals=ff❨10.000000000❩) 
│  _result required by _sum ≤ required r_0            equiv id                                        
│  ff required by a         ≤ required ff             equiv id                                        
│  x required by a          ≤ required x              equiv (always satisfied)                        
├  _lim: SimpleWrap                                                                                   
│        │  provides   _l   {10 m} │ -                                                                
│        └ DP_Limit {10 m}  ⇸  𝟙  > NVU:10 m                                                          
│           𝒇 ≤ 10 m                                                                                  
├ _lim1: SimpleWrap                                                                                   
│        │  provides   _l1   {100 m} │ -                                                              
│        └ DP_Limit {100 m}  ⇸  𝟙  > NVU:100 m                                                        
│           𝒇 ≤ 100 m                                                                                 
├ _plus: SimpleWrap                                                                                   
│        │  provides   _op   SB(≥0) m │ requires   _res   SB(≥0.1) m                                  
│        └ DP_L_UME SB(≥0) m  ⇸  SB(≥0.1) m                                                           
│           𝒇 + 0.1 ≤ 𝒓                                                                               
│          M_C_WrapUnits   m → m > M_A_Add1_Upper   SB(≥0)  →  SB(≥0.1) x ⟼ x + 0.1                   
├  _sum: SimpleWrap                                                                                   
│        │  provides   f_1   SB(≥0) m │ requires   _result   SB(≥0) m                                 
│        │  provides   f_2   SB(≥0) m │                                                               
│        └ M_Res_AddMany_DP SB(≥0)×SB(≥0) ⟨m,m⟩  ⇸  SB(≥0) m                                          
│           𝒇₁ + 𝒇₂ ≤ 𝒓                                                                               
│          ├      Fs: ├ SB(≥0) m                                                                      
│          │          └ SB(≥0) m                                                                      
│          ├ opspace: SB(≥0) m                                                                        
│          └    algo: ApproximationAlgorithms - ApproximationAlgorithms.VAN_DER_CORPUT                
└     a: CompositeNDP                                                                                 
         │    provides   ff   SB(≥0) m │ requires   ff   SB(≥0) m                                     
         │                             │ requires   x    {1 m}                                        
         │  5 nodes, 3 edges                                                                          
         │   connected rec: ✓                                                                         
         │  _c required by _c      ≤ required x              equiv (always satisfied)                 
         │  provided ff            ≤ _op provided by _mult   equiv id                                 
         │  _res required by _mult ≤ required ff             equiv id                                 
         ├    _c: SimpleWrap                                                                          
         │        │  - │ requires   _c   {1 m}                                                        
         │        └ DP_Constant 𝟙  ⇸  {1 m}                                                           
         │           1 m ≤ 𝒓                                                                          
         └ _mult: SimpleWrap                                                                          
                  │  provides   _op   SB(≥0) m │ requires   _res   SB(≥0) m                           
                  └ DP_L_UME SB(≥0) m  ⇸  SB(≥0) m                                                    
                     𝒇 ⋅ 2 ≤ 𝒓                                                                        
                    M_C_WrapUnits   m → m > M_A_Mult1_Upper   SB(≥0)  →   same x ⟼ x ⋅ 2